next up previous
Next: What good is it? Up: Larch/C++ An Interface Specification Previous: A Sample Trait

A client function

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.


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

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.


next up previous
Next: What good is it? Up: Larch/C++ An Interface Specification Previous: A Sample Trait
Gary T. Leavens
1999-01-26