2.9 Satisfaction

The meaning of a Larch/C++ specification module is a set of C++ code and header files that satisfy it. (This set may be empty if one cannot write a C++ module to satisfy the specification.) A C++ header (`.h') file, and an optional C++ code (`.C', `.cc', etc.) file, satisfy their specification if and only if the following conditions hold.

• The header file contains as code all the C++ declarations specified (with the exception of spec-decls, see section 9.1 Ghost Variables), and C++ declarations for each of the definitions specified (including all classes specified).
• For each function, class, etc., definition specified, the code file contains a C++ definition that satisfies the specification of that function, class, etc. The appropriate notions of satisfaction are described in the bulk of this manual. Note that the code file may obtain some or all of the specified implementations by including the header file. If no implementations are called for, then the C++ code file may be omitted.
• The C++ header file, and the C++ code file when present, are legal C++ code.
• The C++ header file can be legally included by multiple modules in a single program. Thus the header file should not, usually, contain code for C++ functions and the member functions of classes. (An exception would be for inline functions.) Also the header file should not contain a definition of a global variable. (It should only contain a declaration of such.)

If a header file and an optional code file satisfies a specification S, then we say that they implement S, or for emphasis, that they correctly implement S.

The reason for using both a header and a code file (the latter only if needed) to implement each Larch/C++ specification is to promote reuse of C++ code. Thus each C++ implementation has a header file which can be included by other C++ program parts to obtain the declarations of interface. This makes it easier to get the C++ types correct. The Larch/C++ release has several examples of such code with implementations.

Go to the first, previous, next, last section, table of contents.