Vocabulary for Specifying Quadrilaterals

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

  

Figure 1: The LSL trait FourSidedFigure (file FourSidedFigure.lsl).

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.

  

Figure 2: The LSL trait PreVectorSig, which can be used if the type Vec[T] is to be treated as a ``given'' (file PreVectorSig.lsl).

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

  

Figure 3: The LSL trait PreVector (file PreVector.lsl).

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

  

Figure 4: The LSL trait PreVectorSpace (file PreVectorSpace.lsl).

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