next up previous index
Next: Acknowledgements Up: AN OVERVIEW OF LARCH/C++: Previous: Other Subtypes of QuadShape

Discussion and Conclusions

The shapes example from Object Orientation in Z [45] is perhaps not ideal for illustrating the mechanisms in Larch/C++ used for specification inheritance, as the subtypes all use the same set of specification variables and no member function specifications are strengthened. In our other work [11,30], we give more interesting examples, in which the abstract models of the subtype objects contain more information than objects of their supertypes.

However, the shapes example does permit direct comparison to the OO specification languages presented in Object Orientation in Z [45]. The following are the most basic points of similarity and difference.

  It is important that a formal specification language not require one to formalize every detail. By allowing one to leave some types of data, some operations, and some aspects of behavior informal, Larch/C++, like Z and other OO specification languages, allows users to focus on what is important. In LSL, informality is accomplished by omitting specifications, as in Figure 2. In Larch/C++ informality can also be accomplished by omitting specifications as in Figure 6, but more fine-grained tuning is permitted by the use of the informal predicates.

    Larch/C++ is a large, but expressive, specification language. Most of its size and complexity arises from the complexity of C++, which, for example, has a large and complex declaration syntax, and a large number of low-level, built-in types. Although Larch/C++ has several features that other formal specification languages do not have, these features earn their place by adding much to the expressiveness of the language. For instance, the requires redundantly, example, and ensures redundantly clauses in function specifications add syntax, but they allow additional checking and also allow one to convey extra information about the meaning and intent of a specification. The requires redundantly and example clauses are new with Larch/C++; the idea for the ensures redundantly clause and redundancy in interface specifications is due to Tan [48,47,49]. (Tan called this a claims clause.)

More important for expressiveness are some fundamental semantic ideas that, while they also add to the complexity of the language, add new dimensions to the expressiveness of the language. One semantic idea is the distinction between trashing and modification [7,8], which places the frame axiom of Larch-style specification languages on a firm semantic foundation. In Larch/C++ one can also specify such notions as whether storage is allocated or assigned. More important, allowing the user to specify both total and partial correctness for functions gives to users a choice previously reserved by specification language designers; the use of partial correctness, for example, is necessary for succinct specification of functions that may fail due to the finiteness of various data structures [19]. Allowing the specification of several specification cases (an idea due to Wing [54, Section 4.1.4] and Wills [50,51,52]) is convenient for the specification of exceptions and for giving a concrete form to specification inheritance [11]. Furthermore, when combined with the ability to specify both total and partial correctness, the expressiveness of the specification language becomes much more complete [18].

The Larch approach of behavioral interface specification [54,53], and the expressive features of Larch/C++ make it a step towards the more practical and useful formal documentation for object-oriented classes.


next up previous index
Next: Acknowledgements Up: AN OVERVIEW OF LARCH/C++: Previous: Other Subtypes of QuadShape
Gary T. Leavens
1999-01-26