next up previous
Next: Specification of Classes Up: Larch/C++ An Interface Specification Previous: What is Larch/C++?


The notion of satisfaction says when a C++ function satisfies a Larch/C++ specification. Consider the specification in Figure 2.

Figure 2: The Larch/C++ specification of the C++ function sqrt (file sqrt.h).
\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush...{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex}

Note that this specification doesn't give an algorithm for computing the square root of an integer.

The specification in Figure 2 is satisfied by a C++ function that has:

In the example, the interface is given on the first line. The argument and result have to be C++ ints.

What it does, its behavior, is given by the lines starting with //@. The requires clause says what must be true of the argument to call sqrt. The ensures clause says what will be true about the return value, named result. The notation /\ means ``and''.

The predicate following requires is called a precondition, and the one following ensures is called a postcondition.

Gary T. Leavens