The abstract model of a class is used to specify a client function that works on objects of that class. For example, Figure 6 specifies a client function that works on instances of the class Point.
Notice that this specification includes the specification of Point, from the file Point.h. The argument p is passed by reference. Larch/C++ considers a reference parameter to be an object, hence p is an object. As such it has an abstract value both before and after the call. Its abstract value, recall, is made up of two specification variables x and y.
The modifies clause of MoveNE does not allow p to be changed, but, since it is an object, in the Larch/C++ notation, one must write p'.x' to refer to the value of x in the value of p after the call.
Arguments, like d, that are not passed by reference
are considered to be values, not objects.
Hence the ^ and ' notation is not used for d.
A Larch/C++ function specification may optionally include one or more examples. These do not change the meaning of the specification; that is, they are redundant. However, they are useful in making the specification clearer. They also allow one to check the specification for consistency, and may thus be useful in ``debugging'' the specification. They may also be useful in testing an implementation.
