Larch/C++ is a notation for formally specifying the behavior and interfaces of C++ classes and functions. C++ is the programming language defined in Stroustrup's book [Stroustrup91](1) and more fully in Ellis and Stroustrup's book [Ellis-Stroustrup90] and the draft C++ standard [ANSI95]. These contain the reference manual for C++. We will often refer to sections of the reference manual by citing one of these. (These sections are roughly correlated: Section r.7.1 in [Stroustrup91] is the same as Section 7.1 in [Ellis-Stroustrup90].)
The goal of this reference manual is to precisely record the design of Larch/C++. (2) We try to give examples and explanations, and we hope that these will be helpful to readers trying to learn about formal specification using Larch/C++. However, this manual is not designed to give all the background needed to write Larch/C++ specifications, nor to give the prospective user an overview of a useful subset of the language. For this background, we recommend the following. The reader new to formal specification or new to the Larch approach to behavioral interface specification is advised to read chapters 1-4 of [Guttag-Horning93] first. Such a reader might also want to consult [Leavens98], where more tutorial material on Larch can be found. Once the reader has the necessary background, an overview of a useful subset of Larch/C++ can be found in the paper [Leavens96]. There is also a "poster" that ships with the release. (A useful, but somewhat obsolete overview can also be found in [Cheon-Leavens94].)
Readers with the necessary background, and users wanting more details may, we hope, profit from reading this manual. We suggest reading in this manual starting with chapters 1-3, skimming chapter 4 quickly, skimming chapter 5 to get the idea of what declarations mean in Larch/C++ (paying a bit more attention in section 5.4 to the sorts of declarations), and then reading the chapters on function and class specifications, paying particular attention to the examples. After that, one can use the rest of this manual as a reference.
Go to the first, previous, next, last section, table of contents.