LSL Traits Specify Mathematical Vocabulary

In the precondition of the member function Move of Figure 3, the notation inRange(x^ + dx) is used. In a formal specification language, like Larch/C++, such notation must have a well-defined meaning.

In a Larch-style behavioral interface specification language (BISL), the meaning of symbols like inRange, +, and /\ is specified formally in a module of the Larch Shared Language (LSL), called a trait. Each Larch-style BISL, such as Larch/C++, Larch/Smalltalk, or Larch/Ada, uses LSL traits to specify the notation used in its pre- and postconditions.

Thus, the big picture is as in Figure 4. This shows that:

• LSL traits specify the abstract model, i.e., the mathematical vocabulary for describing abstract values.

• Larch/C++ specifies the interface and behavior using pre- and postconditions written in terms of this vocabulary.

• Clients can reason about C++ functions using the pre- and postconditions.

  

Figure 4: The layers of a behavioral interface specification.

The mathematical operations specified in the trait are only used in writing the assertions; they can't be used in programs. To ensure that the assertions are well-defined, they can't call C++ code. (If an assertion used C++ code, one couldn't easily interpret expressions used in assertions as abstract values, because C++ code doesn't deal with mathematical entities.)

The idea of specifying and reasoning using abstract values goes back to Hoare's 1972 paper ``Proof of correctness of data representations'' (Acta Informatica, Vol 1, Num. 4).