Larch

        The work of Wing, Guttag, and Horning on Larch extends the VDM-SL and Z tradition in two directions [54,53,16]:

•     Although a mathematical toolkit is provided [16, Appendix A], specifiers may design their own mathematical theories using the Larch Shared Language (LSL) [16, Chapter 4]. This allows users, if they desire, to create and use an abstract model at exactly the right level of abstraction; that is, one can either build an abstract model out of readily available parts, or one can build a model from scratch. Clearly, not everyone should be building models from scratch; thus it is convenient that those that do get built can be shared, even among users of different behavioral interface specification languages.

•                                   Instead of one generic specification language, there are several behavioral interface specification languages (BISLs), each tailored to specifying modules to be written in a specific programming language. Examples include LCL [16, Chapter 5] (for C), LM3 [16, Chapter 6] (for Modula-3), Larch/Ada [15] (for Ada), Larch/CLU [54,53] (for CLU), Larch/Smalltalk [9] (for Smalltalk) and Larch/C++.

The advantage of tailoring each BISL to a specific programming language is that one can specify both the behavior and the exact interface to be programmed [22]. This is of great practical benefit, because the details of the interface that need to be specified vary among programming languages. For example, because Larch/C++ is tailored to the specification of C++ code, it allows users to specify the use of such C++ features as virtual, const, exception handling, and exact details of the C++ types (including distinctions between types such as int and long int, pointers and pointers to constant objects, etc.). No such details can be specified directly in a specification language such as VDM-SL or Z that is not tailored to C++. The same remark applies to object-oriented (OO) specification languages such as Z++ [25,24], ZEST [10], Object-Z [41,42], OOZE [1,2,3], MooZ [37,38], and VDM++ [39]. However, apparently there are ``variants of Fresco'' [50,52] that are ``derived from C++ and Smalltalk'' [51, p. 135]; these may permit more exact specification of interface details.

The remainder of this paper gives a set of examples in Larch/C++, and then concludes with a discussion. The set of examples specifies a hierarchy of shapes that is used as a case study in the book Object Orientation in Z [45]. An index is provided for important ideas and examples.