Following the ZEST [10] and Fresco [51] specifications of the shapes example, the first class to specify is an abstract class of four-sided figures, QuadShape. The reason for this is that, if we follow [45, Chapter 2], then quadrilaterals are shearable, but some subtypes (rectangle, rhombus, and square) are not. If we were to follow the class hierarchy given on page 8 of Object Orientation in Z [45], there would be problems, because the classes Rectangle, Rhombus, and Square would be subtypes but not behavioral subtypes of the types of their superclasses. Informally, a type S is a behavioral subtype of T if objects of type Scan act as if they are objects of type T[4,5,31,26,36,32]. Having subclasses not implement subtypes would make for a poor design; it would also make such classes unimplementable if specified in Larch/C++. This is because Larch/C++ forces subclasses to specify behavioral subtypes of the types of their public superclasses [11]. Thus we will follow the ZEST and Fresco specifications in using an abstract class without a shear operation as the superclass of Quadrilateral.
The Larch/C++ specification of the abstract class QuadShape is given in Figure 5. This behavioral interface specification includes the behavioral interface specifications of the type Vector, which itself includes the specification of the type Scalar. In Larch/C++, one could also specify QuadShape as a C++ template class with the types Vector and Scalar as type parameters [30, Chapter 8], but the approach adopted here is more in keeping with the examples in Object Orientation in Z [45].
In the specification of QuadShape, the first thing to note is that the syntax that is not in comments is the same as in C++. Indeed, all of the C++ declaration syntax (with a few ambiguities removed) is supported by Larch/C++. A C++ declaration form in a Larch/C++ specification means that a correct implementation must be C++ code with a matching declaration. (Hence, a Larch/C++ specification cannot be correctly implemented in Ada or Smalltalk.) This happens automatically if, as in these examples, the behavioral specifications are added as annotations to a C++ header file.
Annotations in Larch/C++ take the form of special comments. What to C++ looks like a comment of the form //@ ... or /*@ ... @*/ is taken as an annotation by Larch/C++. That is, Larch/C++ simply ignores the annotation markers //@, /*@, and @*/; the text inside what to C++ looks like a comment is thus significant to Larch/C++.
With such annotations, the user of Larch/C++ can specify semantic modeling information and behavior. At the class level, this is done with the keywords ABSTRACT, uses, and invariant; at the level of C++ member function specifications this is done with the keywords behavior, requires, requires redundantly, modifies, trashes, ensures, example, and ensures redundantly.
Traits that define the vocabulary used in the specification are noted in uses clauses. In the specification of QuadShape, the trait used is FourSidedFigure, In Figure 5, the uses clause precedes the class definition, so that the trait will be available to clients that include QuadShape.h. (A uses clause within the class definition has a scope that is limited to that class.)
The use of the keyword ABSTRACT in the specification of the class QuadShape, specifies the intent that QuadShape is not to be used to make objects; that is, QuadShape is an abstract class. As such, it has no ``constructors'' and therefore no objects will exist that are direct instances of such a class. This extra information could be used in consistency checking tools [48,47,49].
The specification variables edges and position together describe the abstract model of QuadShape values. (As in C++, public: starts the public part of a class specification.) As noted above, because they use the keyword spec, they do not need to be implemented. (An alternative specification would be to use a LSL trait that described the abstract model directly. This was done in the original version of this paper [29], and can be seen in other examples below.)
The invariant clause will be explained following the explanation of the member function specifications.
Each member function specification looks like a C++ member function declaration, followed by a specification of the function's behavior. The the keyword behavior starts the behavioral part. As previously mentioned, use of the C++ declaration syntax allows all of the C++ function declaration syntax, including virtual, const, and throw to be used. It also allows exact C++ type information to be recorded.
To illustrate most of the specification format, the behavioral specification of Move has seven clauses. The requires clause gives the function's precondition, the requires redundantly clause states a redundant property that must hold when the function is called, the modifies and trashes clauses form a frame axiom [6], the ensures clause gives the function's postcondition, the example clause gives a redundant example of its execution, and the ensures redundantly clause states a redundant property of the specification.
The postcondition, and the assertions in the example and ensures redundantly
clauses, are predicates over two states.
These states are the state just before the function body's execution,
called the pre-state,
and the state just before the function body returns (or throws an exception),
called the post-state.
A C++ object (a location) can be thought of as a box,
with contents that may differ in different states.
The box may also be empty.
When the box empty, the object is said to be
unassigned;
an object is assigned when it contains a proper value.
C++ objects are formally modeled in Larch/C++ using various traits
[30, Section 2.8],
and these traits allow one to write assigned(v, pre),
as in the precondition of Move,
to assert that the object v is allocated and assigned in the pre-state.
(The pre- and post-states are reified in Larch/C++ using the keywords
pre and post.)
There is also a more useful notation for extracting the value
of an assigned object in either state.
The value of an assigned object, o, in the pre-state
is written o^ (or o\pre),
and the post-state value of o is written o' (or o\post).
Within a member function specification, data members of class instances are objects, as are arguments passed by reference. This includes specification variables. For example, in QuadShape, both edges and position are considered to be objects. Thus the postcondition of Move says that the post-state value of position is equal to the pre-state value of position plus the pre-state value of the vector v.
The requires redundantly clause is an example of checkable redundancy
[48,47,49].
It allows one to state preconditions that will be true because
they are implied by the stated precondition,
the invariant, or by the semantics of Larch/C++.
What would be checked is that the given precondition,
and the relevant theory of the invariants and parts of the semantics
of Larch/C++ imply the stated assertion.
For example, the first two conjuncts
of Move's requires redundantly clause
say that the specification variables edges and position
are assigned in the pre-state.
(The notation /\ means ``and''.)
This highlights the semantics of Larch/C++, which implicitly
requires that all data members
be assigned in visible states [30, Section 6.2.2].
(The pre-state of a constructor, and the post-state of a destructor are
not considered visible states, and so are exempt from this requirement.)
The last conjunct says that the invariant holds in the pre-state.
The requires redundantly clause is new with Larch/C++.
The ensures clause of Move's specification uses the Larch/C++ keyword liberally. This makes it a partial correctness specification; that is, the specification says that if v is assigned and if the execution of Move terminates, then the post-state must be as specified. However, the function need not always terminate; for example, it might abort the program if the numbers representing the new position would be too large to represent.
If liberally is omitted, then a total correctness interpretation is used; for example, GetPosition must terminate whenever it is called. (Throwing an exception is considered termination, only abortion of the program or infinite loops constitute nontermination.) Neither VDM, Z, nor any other OO specification language that we know of permit mixing total and partial correctness in this manner.
A function may modify an allocated object by changing its value from one proper value to another, or from unassigned to some proper value. Each object that a function is allowed to modify must be noted by that function's modifies clause3. For example, Move is allowed to modify position. An omitted modifies clause means that no objects are allowed to be modified. For example, GetVec and GetPosition cannot modify any objects.
A function may trash an object by making it either become deallocated or by making its value be unassigned. The syntax trashes nothing means that no object can be trashed, and is the default meaning for the trashes clause when it is omitted, as in GetVec and GetPosition. Noting an object in the trashes clause allows the object be trashed, but does not mandate it (just as the modifies clause allows modification but does not mandate it).
Having a distinction between modification and trashing may seem counterintuitive, but is important in helping shorten the specifications users have to write. In older versions of LCL and other Larch interface languages, these notions were not separated, which led to semantic problems [7,8]. By following Chalin's ideas, most Larch/C++ function specifications do not have to make assertions about whether objects are allocated and assigned in postconditions. This is because, unless an object is named in the trashes clause, it must remain allocated if it was allocated in the pre-state, and if it was assigned in the pre-state, then it must also remain assigned in the post-state [30, Section 6.2.3].
An example clause adds checkable redundancy to a specification. There may be several examples listed in a single function specification in Larch/C++. For each example, what is checked is roughly that the example's assertion, together with the precondition should imply the postcondition [30, Section 6.8]. As far as we know, this idea of adding examples to formal function specifications is new in Larch/C++.
Another instance of the checkable redundancy idea is the ensures redundantly clause. This is taken from Tan's work on LCL [48,47,49], where the idea of this kind of checkable redundancy in behavioral interface specifications first appeared. A ensures redundantly clause can be used to state a redundantly checkable property implied by the conjunction of the precondition, the contributions to the postcondition of the frame axioms, and the postcondition. In this case, the claim follows from the frame axioms, as edges cannot be modified.
All of these parts of a function's behavioral specification are optional, except for the ensures clause. This is illustrated by the specification of GetPosition. When the requires clause is omitted it defaults to requires true. (Of course, one can also omit the behavioral specification as a whole.)
In the specification of GetVec, i is passed by value.
Thus i is not considered an object within the specification.
This is why i denotes an int value,
and why notations such as i^ are not used
[16, Chapter 5].
The invariant clause (found just before Move's specification)
describes a property
that must be true of each assigned object of type QuadShape
in each visible state [40];
it can also be thought of as restricting the space of values for the class.
The notation edges\any stands for the abstract value of edges
in any visible state.
Thus the invariant in Figure 5 says
that the value of the edges array in each visible state must form a loop.
Note that, by using model-based specifications, it is easy to specify abstract classes. One imagines that objects that satisfy the specification have abstract values, even though there are no constructors. The use of specification variables (or LSL traits) allows one to describe the abstract values, even though an implementation might have no data members. One can think of these as describing the abstract values of concrete subtype objects.
The type Vector does not have to be fully specified in Larch/C++ in order to be included in the specification of QuadShape. It can be regarded as ``given'' by making a specification module for it that simply declares the type Vector, and uses the appropriate traits. An example of how to do this is shown in Figure 6. (Since the class Vector is declared using the keyword spec, an implementation does not have to declare it as a class, but might define Vector with a typedef or in some other way.) Using a trait, in this case PreVector(Scalar, Vector for Vec[T]) that specifies something with the same name (Vector), tells Larch/C++ about the abstract model of Vector. That is, if v is a Vector object, then the abstract value of v in some state is described by the type Vector specified in the used traits.
In Larch/C++, several syntactic sugars depend on the ability to extract objects that may be within an abstract value. The operator contained_objects must be specified for each type whose abstract values are explicitly modeled by the user in order to make these sugars work. For types like Vector, whose abstract values do not contain any objects, one can do this by simply including an instance of the trait NoContainedObjects [30, Section 7.5] to specify contained_objects in a way that says there are no subobjects in the abstract values.
The same trick for treating Vector as a given type is also used for the type Scalar. Its specification is given in Figure 7. The trait that it uses is given in Figure 8.
The specification of the subclass Quadrilateral is given in Figure 9. The C++ syntax ``: virtual public QuadShape'' is what says that Quadrilateral is a public subclass (and hence a subtype) of QuadShape. (The keyword virtual, in C++, allows multiple inheritors to share a single copy of the data members; this also holds in Larch/C++ for specification variables.) In Larch/C++, a subclass is forced to be a behavioral subtype of the type of its public superclass. Roughly speaking, the idea is that the specification of each virtual member function of QuadShape must be satisfied by a correct implementation of that virtual member function in the class Quadrilateral.
Technically, in Larch/C++ behavioral subtyping is forced by inheriting the specification of the supertype's invariant and virtual member functions in the subtype [11]. Since we have used specification variables in this example, and since these are inherited as in C++, the virtual member function specifications of the supertype, QuadShape, are easy to apply to the subtype. In such examples, one just forgets about extra data members in the subtype when interpreting part of a specification inherited from the supertype. This is also the case in other OO specification languages, including Object-Z [41,42], MooZ [37,38], VDM++ [39], Z++ [25,24], OOZE [1,2,3], and ZEST [10].
(In Larch/C++, and in other Larch-style BISLs, such as LM3 [16, Chapter 6], and Larch/Smalltalk [9], abstract models do not have to be given by specification variables4. For example, in Larch/C++, one can specify a supertype and a subtype and give both of them arbitrary models by writing an LSL trait for each. In such a case, when one does not use specification variables to describe the abstract models of both the subtype and the supertype, giving a semantics to inherited specifications is a problem. See our other work [9,27,11] for how to handle such uncommon cases, and the Larch/C++ reference manual [30] for the details in Larch/C++.)
The ``constructor'' specified for the class Quadrilateral has the same name as the class in C++. Constructors in C++ really are initializers, and this constructor must set the post-state values of the specification variables to the appropriate abstract value. The requires clause is needed so that the object will satisfy the invariant inherited from QuadShape.
The specification of ShearBy illustrates another feature of Larch/C++: informal terms. An informal term starts with the keyword informally and is followed by one or more string constants. An informal term can be used anywhere a boolean term can be used. An informal term can thus be used to selectively suppress details about a specification. This suppression of detail is done frequently in the specifications in Object Orientation in Z [45] by using comments instead of formal specifications when discussing shearing. The use of informal terms is similar, but more tightly integrated, since informal terms can appear within more complex predicates. This example also illustrates how one can use informal predicates to ``tune'' the level of formality in a Larch/C++ specification. For example, in Larch/C++ one could start out by using largely informal specifications, and then increase the level of formality as needed or desired. Informal terms, and their tight integration into Larch/C++, is something that is new with Larch/C++ [29].
The type Shear is specified as a given set in Figure 10. In this example, no signature is given for the trait functions that operate on the type Shear, because that type is only used informally. Using the trait NoContainedObjects(Shear) is enough to tell Larch/C++ that the abstract values are explicitly specified.
