C++ classes can be specified by specifying how the member functions affect various specification variables. Specification variables are data members declared with spec declarations. For example, consider the specification in Figure 3 (the notation is explained below).
In Figure 3, again the lines that are not annotations are part of the C++ interface specification. In the first annotation comment, two specification variables, x and y, are declared. The abstract model of points thus includes two integer objects. These do not have to be part of a correct implementation, but are here just for the purpose of explaining the behavior of the functions.
The first function specified is the constructor. Its job in C++ is to initialize the data members of the class. In this case, it says that the initial values of the actual data members must be such that the object behaves as if its specification variables, x and y, have the values given.
In a function specification, the modifies clause tells what objects or variables can have their values changed by a call. In the constructor, both specification variables can be changed.
A variable, such as x, that can be changed by a call
may have one value x^ just before the call,
and another x' at the end of the call.
See the postcondition of Move for an example that uses both
these notations.
The destructor's specification says that it always returns; that is, it does not do anything necessarily, but always terminates. (Recall that C++ itself recovers the space in stack-allocated objects.)
