C.1 Differences Between Larch/C++ and Larch/C

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.

• The abstract data type mechanism of LCL is not supported in Larch/C++. Use class specifications (see section 7 Class Specifications) instead.
• The semantics of the modifies-clause is different in Larch/C++.
• There is no provision for implicit constraints on names declared as typedefs in Larch/C++.
• The syntax for declaring globals threatened by a function specification is different in LCL than in Larch/C++ (see section 6.7 Global Variables), and no longer required in Larch/C++.
• The syntax -> is not built in as a selection with a defined semantics in Larch/C++ (see section 6.1.9 Primary Suffixes).
• The model for the basic C++ types is different and more detailed in Larch/C++ than in LCL. For example, in Larch/C++ the sort of a formal parameter of type char * is Ptr[Obj[char]] instead of 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 x is a struct declared as a global variable, the meaning of applying a state-function (See section 6.2.1 State Functions) to x is different. In LCL, x^ denotes a tuple of values. In Larch/C++, x^ denotes a tuple of objects. This allows one to say x^.foo to mean the object that is the field named foo in 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).
• Larch/C++ currently supports only the "procedure claims" of LCL in its redundant postconditions; other kinds of LCL claims are not supported and the syntax is different.
• The keyword constraint is used differently in Larch/C++, where it means the history constraints of [Liskov-Wing94].
• There are various differences in the built-in traits of Larch/C++ and LCL.
• The checks clause of LCL is not in Larch/C++.

Go to the first, previous, next, last section, table of contents.