To write a specification in Larch/C++, one specifies an abstract model and mathematical vocabulary, and then uses these to specify the behavior of a C++ interface. The C++ built-in types have models that are supplied by Larch/C++ and written directly in LSL. Users can also directly supply models for objects of their own classes in LSL, but except for classes which are intended to be ``pure values'' like the built-in types, it is often more convenient to specify the model of a class using several specification-only data members. These specification variables are used in the specification, but do not have to be implemented. They often take on values of a type which is not itself intended to be implemented. Examples of both styles of class specification will be given below.
The process of specifying an abstract model and its accompanying vocabulary is not usually completed before one begins writing the behavioral specifications. Quite often, the specifications and the mathematics evolve together, as one searches for better ways to express the desired behavior, and as one better understands what is desired.
To give some examples, this section describes the specification of the abstract class QuadShape and the class Quadrilateral. I first specified QuadShape with 5 specification variables: four vectors representing the sides and a vector giving the position (even this builds on previous work [45]). However, it was more convenient to think of the four edge vectors as components of some structure, so they are modeled as part of an array. Arrays are already modeled by a built-in trait of Larch/C++ [30, Section 11.7], but it was convenient to define some vocabulary (operators) for creating an array of values, and for testing to see whether the vectors in such an array make a loop. In Larch/C++, such vocabulary is specified in a LSL trait. Therefore we turn to traits and the traits used in specifying QuadShape. (See Section2.2 for the Larch/C++ interface specification.)