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:
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).