Larch/C++ is a formal specification language tailored to C++. Its basic use is thus the formal specification of the behavior of C++ program modules. As it is a behavioral interface specification language, Larch/C++ specifies how to use such C++ program modules from within a C++ program; hence Larch/C++ is not designed for specifying the behavior of an entire program. So the question "what is Larch/C++ good for?" really boils down to the following question: what good is formal specification for C++ program modules?
The main benefit in using Larch/C++ is precise, unambiguous documentation
of the behavior C++ program modules (functions, classes, etc.).
A Larch/C++ specification can be a completely formal contract about
an interface and its behavior.
Because it is an interface specification,
one can record all the C++ details about the interface,
such as the parameter mechanisms, whether the function is virtual,
const, etc.;
if one used a specification language such as VDM-SL or Z,
which is not tailored to C++, then one could not record such details
of the interface, which could cause problems in code integration.
One can use Larch/C++ either before coding, or as documentation of the code. (The notation is indifferent to the methodological questions; designing before coding is recommended, but documentation after the fact is better than none.)
Reasons for formal documentation of interfaces and their behavior, using Larch/C++, include the following.
There is one additional benefit from using Larch/C++. It is that Larch/C++ allows one to record not just public interfaces and behavior, but also some detailed design decisions. That is, in Larch/C++, one can specify not just the public interface of a C++ class (see section 2.2 Interfaces), but also behavior of a class's protected and private interfaces (see section 10.3 Specifying Protected and Private Interfaces for more information about how this is done). Formally documenting a base class's protected interface is a step towards the day when users can implement derived classes of such a base class without looking at its code. (There are still other problems to be worked out in this regard, however.) Recording the private interface of a class may be helpful in program development or maintenance. Usually one would expect that the public interface of a class would be specified, and then separate, more refined specifications would be given for use by derived classes and for detailed implementation (and friend classes). (See section 10.2 Class Refinement for how to record each level in Larch/C++.)
Our specific goals for Larch/C++ are as follows [Leavens-Cheon92b].
Originally, it was also a goal of Larch/C++ to have no unmotivated differences from LCL, a specification language for C (see [Guttag-Horning91b] and Chapter 5 of [Guttag-Horning93). This was intended to avoid rethinking various issues in Larch/C++. Larch/C++ owes much of its syntax and semantics to LCL. However, for two reasons Larch/C++ is not compatible with LCL. The main reason is that LCL has a particular way to specify ADTs, and Larch/C++ has a completely different style for specifying C++ classes. This is not just a matter of syntax; LCL has a specific method for designing programs that engenders many design decisions. In particular the way LCL models the built-in types (of C) is influenced by its design method. One aspect of the LCL design method, not needed in C++, is that it overcomes the lack of reference parameters in C. This difference leads to the second major reason Larch/C++ is incompatible with LCL: the models of the built-in C++ types are quite different from the corresponding models in LCL. In general the models used by Larch/C++ are more detailed and more faithful to the semantics of C++ (and C). See section C.1 Differences Between Larch/C++ and Larch/C for a more detailed comparison.
In addition, we have some other goals that are motivated by ideas on object-oriented design [America87] [Meyer88] [Leavens-Weihl90] [Leavens90] [Leavens91] [Leavens-Weihl95]. These ideas use the concept of supertype abstraction, which is the ability to reason about a program based on static (or nominal) type information by letting supertypes stand for all their behavioral subtypes. Informally, a behavioral subtype is a type such that each of its objects acts like some object of its supertypes. Supertype abstraction allows one to reason about a program in terms of these (hypothetical) supertype objects instead of reasoning about the details of the subtype objects. To support supertype abstraction, our goals are as follows [Leavens-Cheon92b].
There is still some work remaining on the second point above, particularly with respect to types with mutable objects (see [Dhara-Leavens94b] [Dhara-Leavens96]).
Go to the first, previous, next, last section, table of contents.