Since Larch/C++ is an interface specification language for C++, and Larch/C (LCL, see Chapter 5 of [Guttag-Horning93]) is an interface specification language for C, a fundamental difference is that an implementation of a Larch/C++ specification must be in C++, while an implementation of a LCL specification must be in ANSI C.
The current version of LCL [Evans96b] focuses on a semantic checker that is like the old "lint" for C, but uses specification information to provide enhanced checking. Larch/C++ is evolving towards something similar, but this version of LCL is essentially incompatible with the current version of Larch/C++.
Compared to the version of LCL described in Chapter 5 of [Guttag-Horning93], Larch/C++ has many additions. Instead of listing all the additions here, this section details the incompatibilities between Larch/C++ and the LCL described in [Tan94], and focuses on the changes one would have to make to a LCL specification to make it into a Larch/C++ specification. The following is a list of the most important of these.
typedefs in Larch/C++.
->is not built in as a selection with a defined semantics in Larch/C++ (see section 6.1.9 Primary Suffixes).
String(see section 11.8 Pointer Types). In general, Larch/C++ models types with abstract values that may contain objects, and does not make any assumptions about how the built-in C++ types are used. An example of the previous point is the following. If
xis a struct declared as a global variable, the meaning of applying a state-function (See section 6.2.1 State Functions) to
xis different. In LCL,
x^denotes a tuple of values. In Larch/C++,
x^denotes a tuple of objects. This allows one to say
x^.footo mean the object that is the field named
fooin the post-state, for example in the modifies clause. (In LCL it may be that the name of a global struct is not considered an object, whereas it is in Larch/C++, see section 11.10 Structure and Class Types.) In Larch/C++, one can write
x^^to mean what is meant by
x^in LCL. As another example, the abstract values of a union object in Larch/C++ are modeled in such as way as to mimic the sharing of storage in a C++ union (see section 11.11 Union Types).
constraintis used differently in Larch/C++, where it means the history constraints of [Liskov-Wing94].
checksclause of LCL is not in Larch/C++.
Go to the first, previous, next, last section, table of contents.