Other Subtypes of QuadShape

This section contains the specifications of the other subtypes of QuadShape described in Object Orientation in Z [45].

As in the ZEST specification of the shapes examples [10], we start with the abstract type ParallelShape, which is shown in Figure 11. The invariant clause in this specification says that the abstract values of such objects must have edges with parallel sides. (The operator isaParallelogram is specified in the trait shown in Figure 12.)

An interesting aspect of ParallelShape (apparently overlooked in all the specifications in Object Orientation in Z [45]) is that if all the sides of a quadrilateral are zero length, then the angle to be returned by AnglePar is not well-defined. The specification of AnglePar illustrates how to specify exceptions to handle such cases. (By specifying an exception, the normal case is allowed to have a stronger precondition, and hence its precondition can protect the postcondition from undefinedness [33].) Note first that the body of AnglePar has two pairs of pre- and postcondition specifications. Larch/C++ actually permits any number of these specification cases in a function specification body; the semantics is that the implementation must satisfy all of them [54, Section 4.1.4] [50,51,52] and that a caller must establish the disjunction of the preconditions. Thus this specification says that if the receiver's edges describe a shape with an interior, the appropriate angle must be returned, and if not, then it must throw the exception NoInterior. (The notations ~ and \/ mean ``not'' and ``or'' respectively.) Although the mathematics of angles is left informal, the specification of the exception is formalized. The term returns is true just when the function returns normally without throwing any exception, and throws(NoInterior) is true just when the function throws an exception of type NoInterior. The claim in the exceptional case shows how one can describe the abstract value of the exception result of a given type. (In this case the claim is trivially true, because there are no other proper values and the exception result is passed by value.)

**Figure 11:** The Larch/C++ specification of the C++ class `ParallelShape` (file `ParallelShape.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

**Figure 12:** The LSL trait `IsaParallelogram` (file `IsaParallelogram.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}$

The specification of the type NoInterior is in Figure 13. This specification uses an instance of the Larch/C++ built-in trait NoInformationExecption [30, Section 6.10] to specify the abstract model of the type NoInterior. This trait is designed as an aid in specifying abstract models for exception types in which no significant information is being passed; it says that there is only one abstract value: theException. The class specification also specifies the default constructor. In Larch/C++, the keyword self denotes the object that C++ programs refer to as *this; that is, self is a name for the object being constructed (or the object receiving a message in a member function). In a specification where the abstract model is given explicitly by an LSL trait (in this case by the first trait used), the value of self' is one of the values described in that trait.

**Figure 13:** The Larch/C++ specification of the C++ class `NoInterior` (file `NoInterior.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

Turning to another concrete class specification, the type Parallelogram (see Figure 14) is a public subclass of both Quadrilateral and ParallelShape. (This follows the design in Object Orientation in Z [45]; whether this is a good idea for a design in C++ is debatable.) It inherits the specifications of each, including the ShearBy member function of Quadrilateral, and the invariant from ParallelShape (including the inherited invariant from QuadShape). This is done by specifying a simulation function for each supertype. Of course, the constructor of Quadrilateral is not inherited, and so a constructor must be specified. This specification is a partial correctness specification, which allows for cases in which the vector cannot be successfully negated.

**Figure 14:** The Larch/C++ specification of the C++ class `Parallelogram` (file `Parallelogram.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

Another shape type is Rhombus, which is specified in Figure 15. This class is specified as a public subclass of ParallelShape. The trait used to specify the operator isaRhombus is in Figure 16.

**Figure 15:** The Larch/C++ specification of the C++ class `Rhombus` (file `Rhombus.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

**Figure 16:** The LSL trait `IsaRhombus` (file `IsaRhombus.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}$

The class Rectangle is specified in Figure 17. Its invariant is specified using the trait IsaRectangle from Figure 18.

**Figure 17:** The Larch/C++ specification of the C++ class `Rectangle` (file `Rectangle.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

**Figure 18:** The trait `IsaRectangle` (file `IsaRectangle.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}$

Finally, in Figure 19 the class Square is specified as a public subclass of both Rhombus and Rectangle. The trait IsaSquare, given in Figure 20, is used in the specification of the constructor to state a claim that follows from the inherited invariant, but which might not otherwise be obvious.

**Figure 19:** The Larch/C++ specification of the C++ class `Square` (file `Square.h`).
$\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush... ...in{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex} \end{figure}$

**Figure 20:** The LSL trait `IsaSquare` (file `IsaSquare.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}$