A Sample Trait

The functions specified in traits are called trait functions. For example, inRange, used in the specification of Point's Move function is a trait function, as is + and /\. Each of these is defined in an LSL trait. Users typically do not have to write the specifications of many trait functions, since lots of them are standard in LSL and others are built-in to Larch/C++.

Figure 5 is a (simplified) version of the LSL trait int that defines the meaning of various trait functions that work on the C++ type int, including inRange and +.

**Figure 5:** A simplified version of the LSL trait `int` (file `int.lsl`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

This trait includes the following trait instances: Integer(int), Between(int), and NoContainedObjects(int). Each of these is a copy of another trait, with the name int replacing their first parameter. (For example, int replaces Int in the trait Integer when the notation Integer(int) is used.)

The trait Integer is specified in Guttag and Horning's book Larch: Languages and Tools for Formal Specification (Springer-Verlag, 1993). It describes the theory of integers, and defines the meaning of the trait function + that is used above. This book contains a ``Handbook'' of other useful and standard traits. Using this handbook, Larch/C++ users do not usually have to define traits for basic mathematics or data structures.

The other two included traits in Figure 5 are part of a handbook provided by Larch/C++. The trait Between(int) specifies the trait function between, which says what it means for one integer to be between two others. The trait NoContainedObjects(int) says that the values of type int do not have subobjects; it is a detail that can be ignored for now.

Returning to the trait int in Figure 5, there are three sections following the includes section. The first of these, the introduces section, declares the signatures (types) of the trait functions INT_MIN, INT_MAX, and inRange. The first two, since they have no arguments, are effectively constants.

The second, the asserts section, specifies some axioms that define the meaning of these trait functions. You might notice that INT_MAX is not precisely specified, this is okay, as the C++ standard does not precisely specify it either.

The last, the implies section, redundantly states a consequence of the theory specified in the asserts section. Such redundancy is useful in ``debugging'' the trait.

Although usually one does not have to develop complicated traits from scratch, the ability to specify new traits allows one to specify with a vocabulary that is exactly suited to an application, if desired.