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
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 +.
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
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.