Although LSL has the power to specify abstract models ``from scratch,'' most abstract models are built using tuples (records), sets, and other standard mathematical tools that are either built-in to LSL or found in Guttag and Horning's Handbook [16, Appendix A].

A typical example is given in Figure 1.
That figure specifies a theory in LSL,
using a LSL module, which is called a *trait*.
This trait is named `FourSidedFigure`, and has a parameter `Scalar`,
which can be replaced by another type name when the trait is used.
This trait itself includes instances of:
`PreVector(Scalar, Vector for Vec[T])`, `int`,
and `Val_Array(Vector)`.
The first of these gives part of the model for vectors,
and will be discussed further below.
The second of these gives a model for the C++ type `int`
with appropriate auxiliary definitions for C++
[30, Section 11.1.5].
The last of these gives a model for the abstract values of C++ arrays
of vectors
[30, Section 11.7].
This model includes such operations as indexing into an array
using the `__[__]`

operator.
(LSL uses the notation `__`

to
indicate the places where arguments to mixfix operators can be passed.
For example, one can obtain the element at index 3 of an array value `e`
by writing `e[3]`.)
The LSL name for this type (sometimes called a *sort*)
is `Arr[Vector]`.

The trait `Val_Array` has a type parameter, the type of its elements,
and the actual parameter, `Vector`, replaces it.
Thus the trait `Val_Array(Vector)` can be thought of as a
copy of the trait `Val_Array`, with the name `Vector` replacing
the formal sort parameter of `Val_Array`.
The trait `PreVector(Scalar, Vector for Vec[T])`
is a copy of `PreVector` with the name `Scalar` replacing
its parameter (`T`), and with the name `Vector` replacing `Vec[T]`.
(These replacements are done simultaneously.)

Returning to Figure 1,
in the lines following `introduces`,
the signatures of two operators are specified.
Their theory is specified in the lines following `asserts`,
and (what are intended to be) redundant consequences of this theory
are specified in the lines following `implies`.

In the `asserts` section,
the specification defines an operator, `isLoop`,
to test whether four vectors define a four-sided figure
[45, Section 2.2.3].
The term `isLoop(e)` is true just when
the vectors in the array value `e` sum to zero (make a loop).
It is specified using the `+` operator from the trait
`PreVector(Scalar, Vector for Vec[T])`.
(It would be inconsistent (i.e., wrong) to simply assert that
the edges always sum to zero; doing so would assert that
all combinations of four vectors in an array value sum to zero,
but array values can be constructed so that this does not hold.
Such properties must be handled by either constructing an abstract
model from scratch, or by asserting that the property holds at
the interface level, as is done in the interface specification
of `QuadShape` below.)

In the `asserts` section,
the operator `\<__,__,__,__\>`

is specified to make an
array value from its four arguments.
It is specified using the `assign` operator on
array values from the trait `Val_Array(Vector)`.

The `implies` section of Figure 1
illustrates an important feature
of the Larch approach:
the incorporation of checkable redundancy into specifications.
The first part of the `implies` section states some theorems
about the operators introduced in the `asserts` section.
The second part says that the two operators specified are well-defined
relative to other operators.
Such redundancy can serve as a consistency check;
it can also highlight consequences of the specification
for the benefit of readers.
One can attempt to formally prove that the theory stated in the `implies`
section follows from the rest of the specification using a theorem prover,
and that may be helpful in ``debugging'' the specification
[16, Chapter 7].

In *Object Orientation in Z* [45],
vectors are usually treated as a *given set*,
meaning that their specification is of no interest.
A type of values can be treated as a given set in LSL
by simply specifying the signatures
of its operators that are needed in other parts of the specification,
without giving any assertions about their behavior.
For example, to treat vectors as a given set,
one would have `FourSidedFigure` include
the trait `PreVectorSig`,
as specified in Figure 2,
instead of `PreVector`.
Comments, which start with `%`

and continue to the end of a line,
can be used to give some informal description of these operators if desired.

Although it is perfectly acceptable to treat
vectors as a given set (and beginning users are encouraged to
make similar simplifications to avoid mathematical difficulties),
one can obtain a more precise specification
(and illustrate more of the power of LSL)
by fleshing out the trait `PreVector`.
This is done in Figure 3.

The trait `PreVector` specifies an abstract model
of vectors.
This trait specifies the type `Vec[T]` with an approximate `length`
operator^{2}.
Recall that the trait `FourSidedFigure`
copies this trait and changes the names `Vec[T]` to `Vector`
and `T` to `Scalar`.
Such differences in naming are common when reusing traits
designed for other purposes, such as `PreVector`.

In the `assumes` clause of `PreVector`,
the type `T` is required to be a ring with a unit element,
have a commutative multiplication operator (`*`), be totally ordered,
and have conversions to and from the real numbers.
(The first three assumed traits are found in
[16, Appendix A]; the last trait, and the included trait
`Real` that specifies the real numbers,
are found in [28].)
The use of traits for stating such assumptions
is similar to the way that theories are used for parameterized specifications
in OBJ [14,13].
The assertions in the trait `PreVector`
specify the theory of an inner product and the approximate length function.

In the `implies` of `PreVector`,
the naming of another trait, in this case `PreVectorSig(T)`,
says that the theory of that trait is included in this trait's theory.
`PreVector`'s `converts`
clause says that there is no ambiguity in the specification of
the inner product operator.
However, note that the `length` operator is not so well-specified,
and thus is not named in the `converts` clause.

To push this mathematical modeling back to standard traits,
the trait `PreVectorSpace`, found
in Figure 4, is used.
(The trait `DistributiveRingAction` is found in
[28], the other traits are from
[16, Appendix A].)

Now that we are done with the initial mathematical modeling, we can turn to the behavioral interface specifications.

1999-01-26