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


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.

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.