The work of Wing, Guttag, and Horning on Larch extends the VDM-SL and Z tradition in two directions [54,53,16]:
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 . 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 , Object-Z [41,42], OOZE [1,2,3], MooZ [37,38], and VDM++ . 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 . An index is provided for important ideas and examples.