Satisfaction

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).

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:

• the same C++ interface (has name sqrt and same types),

• a meaning that conforms to the specification.

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.