The notion of satisfaction says when a C++ function satisfies a Larch/C++ specification. Consider the specification in Figure 2.
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.
/\ means ``and''.
The predicate following requires is called a precondition, and the one following ensures is called a postcondition.