The five object composition primitives in SpecL are just that -- primitive. In particular, using just these five primitives, there is no way to specify any of a number of important properties about objects and operations. For example, in the PersonDatabase object suppose it is necessary to specify that the database cannot have duplicate entries. Or, suppose it is necessary that the database behave as a queue-like structure, such that new records are added on a first-come-first-served (FIFO) basis. Neither of these or similar properties can be defined with the use of composition primitives alone. The use of formal specification is necessary in such cases.

One method to describe properties such as these is to use English. It is in fact useful to describe all properties of an entity in its English description. However, it is not sufficient to rely solely on natural language to specify critical properties. To do so soon leads to well-known problems of ambiguity and imprecision. Therefore, it is necessary to use the more formal language of mathematics to obtain a truly precise and unambiguous specification.

Another method to describe properties is to use a computer programming language. This has the advantage of being fully precise and unambiguous. However, using a programming language for specification is fundamentally contrary to the purpose of specification. Namely, a specification should be as free as possible of implementation detail. The purpose of a programming language is precisely for the expression of implementation detail.

To overcome the disadvantages of English and programming languages, researchers have developed a number of formal techniques expressly for use in specification. The two formal techniques supported primarily in SpecL are algebraic and predicative specification. With the algebraic technique, formal properties are specified as a set of equations associated with an object. Hence, algebraic specifications can be considered object-oriented. In the predicative technique, formal properties are specified as preconditions and postconditions on operations. Hence, predicative specification can be considered operation-oriented.

It is important to note that the two techniques provide different approaches to formal specification. A system can be fully specified using only the algebraic approach, it can be fully specified using only the predicative approach, or it can be specified using a combination of the two approaches.

A potential problem with either of these forms of specification is the introduction of implementation biases into a specification. As examples below illustrate, these formal specification techniques tread a fine line between specification and implementation. In fact, what many software engineers call a specification language others may call a very high-level programming language.

The gist of the problem is that the more precise we try to become with a specification, the more we tend to constrain what the implementation can look like. However, this violates the general principle that a specification is as free from implementation details as possible.

Another problem is that in some cases we find that in order to state a specification sufficiently precisely, we need to interject auxiliary functions, thereby violating the general rule that a specification should contain only entities directly visible to the end user.

In summary, specification is a continual battle between risking imprecision by saying too little versus risking the addition of implementation details by saying too much. The experienced specifier learns how to wage this battle successfully.

8.1. Equational Specification

An equational specification formally defines an object in terms of equations between the operations of the object. Equational specifications are desirable because they require no underlying data model. Rather, the definition of an object is stated entirely in terms of its abstract operations. This model-free property of equational specification is generally not satisfied by other forms of formal specification. For example, the predicative style of specification defined below in Section 8.4 is not model-free. Rather, predicative specification relies on a list-based data model to provide a basis for defining formal preconditions and postconditions. Without reliance on some underlying model, the predicative style of specification would not be complete.

The process of defining an equational specification is divided into three major steps:

1. Define the operation signatures for the object's operations
2. Categorize the operations into constructors, destructors selectors, and initializers
3. Define the equations

To illustrate these steps, consider the definition of a database object that has a set-like structure. That is, it has the property that duplicate entries are not allowed. Here is an equational definition for such a database:

object SetDB is
    components: Elem*;     (* Note the minimal representation *)

    operations:
        Insert: (SetDB, Elem) -> (SetDB),  (* Constructor operation *)
        Delete: (SetDB, Elem) -> (SetDB),  (* Destructor operation *)
        Find: (SetDB, Elem) -> (boolean),  (* Selector operation *)
        EmptyDB: () -> (SetDB);            (* Initializer operation *)

    equations:
        var s: SetDB; e, e': Elem;

        Find(EmptyDB()) == false;
        Find(Insert(s, e), e') ==
            if e=e' then true else Find(s, e');
        Delete(EmptyDB(), e) == EmptyDB();
        Delete(Insert(s, e), e') ==
            if e=e'
            then Delete(s, e')
            else Insert(Delete(s, e'), e);

end SetDB;

The operations section of the SetDB definition contains the full signatures for its operations. The general form of a signature in the operations sections is

operation name : (list of inputs) -> (list of outputs)

Before defining the equations, an object's operations are organized into the following categories:

1. Constructor and initializer operations that build an object out of smaller parts. These two categories can be grouped under the common heading of constructors.
2. Selector and destructor operations that access or remove some component of an object. These two categories can be grouped under the common heading of selectors.
3. Derived operations that can be defined formally in terms of one or more constructors or selectors.

The important characteristic of constructor operations is that they are additive. That is, the resulting output of a constructor is a combination of the inputs. In contrast, selector operations are subtractive. That is, the resulting output is some smaller piece of the input. In general, an equationally defined object should have at least one each of the constructor, initializer, destructor, and selector operations.

Once operations have been fully defined and categorized, the equations themselves are defined. The general format of an equation is the following:

functional_expr == quantifier_free_expression;

The following guidelines are useful for constructing a correct equational specification:

1. The equations define what the selector operations do to the constructor operations, and not vice versa. That is, the outermost operation name in the LHS of an equation should always be a selector, not a constructor.
2. There should be one equation that defines what each selector does to each constructor. Hence, if there are c constructors and s selectors, then there are c * s equations.
3. Equations are defined in an inductive style. Specifically, equations are defined in groups, where the first of the group specifies what a selector does with an initializer. The remaining equations in the inductive group specify what a selector does with the other constructors.

1. The SetDB selectors are Find and Delete. Hence, each of the SetDB equations has one of these as the outermost operation in the LHS of the equation.
2. Since there are 2 selectors and 2 constructors, there are a total of 4 equations.
3. The inductive style of definition indicates that two groups of equations are appropriate. The first group of two equations specifies what Find does to EmptyDB and Insert. The second group of equations specifies what Delete does to EmptyDB and Insert.

To begin, it is assumed that the reader is familiar with the concept of proof by mathematical induction. Readers entirely unfamiliar with this topic should consult an appropriate reference. Recall that an inductive proof is a two step process, in which a proposition p(x) is proved for all values of x. The steps are:

1. Proof of the base case: set x=0 and prove p(x).
2. Proof of the inductive step: assume p(x) is true for x=n and then prove that p(x) is true for x=n+1.

Find(EmptyDB()) == false;

Delete(EmptyDB(), e) == EmptyDB();

The two inductive step equations in the SetDB example are:

        Find(Insert(s, e), e') ==
            if e=e' then true else Find(s, e');

        Delete(Insert(s, e), e') ==
            if e=e'
            then Delete(s, e')
            else Insert(Delete(s, e'), e);

Both of the inductive-step equations use a recursive style of definition. This is very common in inductive-step equations. The recursion always involves some form of conditional, typically an if-then-else. The test of the condition checks the n+1 case, then the recursion handles the other n cases. Consider again the case for Find:

        Find(Insert(s, e), e') ==
            if e=e' then true else Find(s, e');

By far the most difficult equation in the SetDB example is the last one that defines the inductive step for Delete. The equation is not necessarily intuitive in terms of exactly how it defines set-like behavior. An important technique to determine if a set of equations does what we want is to formally test the equations. To gain an understanding of how the last equation works, we will apply this testing technique shortly. Before doing so, we examine some additional equational definitions.

8.2. Some Additional Equational Definitions

The SetDB example defined equations for the database property that duplicate entries are not allowed. Given below are additional equational definitions that specify other database structural properties. These are all properties that are considered appropriate to be known by an end user.

8.2.1. A Bag-Like Object

Suppose the desired definition of database is one that does allow duplicate entries, that is, it behaves like a mathematical bag instead of a set. To obtain the definition of a bag from that of a set, only one change is necessary -- the then clause of the last SetDB equation is changed from

then Delete(s, e')    (* for a set *)

then s               (* for a bag *)

Suppose we choose to define a LIFO DB, that is, a DB that behaves like a stack. A stack is much simpler than a set since no recursive searching is necessary for the selector operation. For a stack, the selector is the Top operation. Here is the equational definition:

object StackDB is
    components: Elem*;

    operations:
        Push: (StackDB, Elem) -> (StackDB), (* constructor operation *)
        Pop: (StackDB) -> (StackDB),        (* destructor operation *)
        Top: (StackDB) -> (Elem),           (* selector operation *)
        EmptyStackDB: () -> (StackDB);      (* initializer operation *)

    equations:
        var s: StackDB; e: Elem;

        Top(EmptyStackDB()) == EmptyElem();
        Top(Push(s, e)) == e;
        Pop(EmptyStackDB) == EmptyStackDB();
        Pop(Push(s, e)) == s;

end StackDB;

Next we consider the definition of a DB with a FIFO property that is, the definition of a queue-like DB. This definition is intermediate in terms of complexity between a SetDB and StackDB.

object QueueDB
    components: Elem*;

    operations:
        Enq: (QueueDB, Elem) -> (QueueDB),  (* constructor operation *)
        Deq: (QueueDB) -> (QueueDB),        (* destructor operation *)
        Front: (QueueDB) -> (Elem),         (* selector operation *)
        EmptyQueueDB: () -> (QueueDB);      (* initializer operation *)

    equations:
        var q: QueueDB; e:Elem;

        Front(EmptyQueueDB()) == EmtpyElem();
        Front(Enq(q, e)) ==
            if q = EmptyQueueDB()
            then EmptyQueueDB()
            else Front(q);
        Deq(EmptyQueueDB) == EmptyQueueDB();
        Deq(Enq(q, e)) ==
            if q = EmptyQueueDB
            then EmptyQueueDB
            else Enq(Deq(q), e);

end QueueDB;

Finally, we consider the definition of a keyed database, in which duplicates are not allowed. The difference between this and SetDB is a more realistic version of the Find operation. No real database would have Find return a boolean. Rather, Find should return a whole element, which would be located by some Key. The following specification defines this form of database. The equations have the same fundamental structure as SetDB, but with the addition of a Key argument where appropriate.

object DB is
    components: Elem*;

    operations:
        Insert: (DB, Key, Elem) -> DB;  (* constructor operation *)
        Delete: (DB, Key) -> (DB);      (* destructor operation *)
        Find: (DB, Key) -> (Elem);      (* selector operation *)
        EmptyDB: () -> (DB);            (* initializer operation *)

    equations:
        var d: DB; e: Elem; k,k': Key;
        Find(EmptyDB, k) == EmptyElem();
        Find(Insert(d, e, k), k') ==
            if k=k' then e else find(d, k');
        Delete(EmptyDB, k) == EmptyDB;
        Delete(Insert(d, e, k), k') ==
            if k=k'
            then Delete(d, k')
            else Insert(Delete(d, k'), k, e);
end DB;

The first step in testing an equational specification is to understand precisely how equationally defined objects are represented. Since an equationally-defined object has no concrete representation, we have no real way to "get our hands on it." We cannot draw a picture of an object that has no concrete representation. The only means to represent such an object is by using its constructor operations.

Consider the representation of SetDB objects. To build a SetDB, the component type Elem must be defined. Assume for simplicity object Elem is defined as a number. Given this, a SetDB object will contain numeric values. As a concrete example, the SetDB containing elements 1, 2, and 3 is represented as a functional expression containing three applications of the Insert constructor:

Insert(Insert(Insert(EmtpyDB(), 1), 2), 3)

To apply a selector operation to a constructed object, the constructed object simply appears as an argument in the appropriate selector argument position. For example, to delete the element 2 for the above set, the Delete operation is applied as follows:

Delete(Insert(Insert(Insert(EmtpyDB(), 1), 2), 3), 2)

The general method to test a set of equations is to consider the equations as reduction rules and apply these rules to a constructed object. In general, a reduction rule is of the form

LHS -> RHS

A reduction rule is said to be applied to some subject. In the case of an equational rewrite rule, the subject is a term. Rewrite rule application involves matching the LHS of the rule to some part of the term, and then replacing the matched term with the RHS of the rule. This replacement of the matched LHS with a RHS is the actual rewriting process.

The goal of equational term reduction is to remove all selector operations from a term, leaving only constructors. This goal makes sense when we consider the form of the equations. Recall that equations are written in terms of what a selector does to a constructor, not the other way around. The reason that we do not define equations for what constructors do is that they need not be reduced. In other words, a term containing only constructors is considered fully reduced. In this way, an actual object is represented fundamentally by a series of constructor operations. Whenever a selector is applied to a constructed object, the selector is "reduced out" to produce a term that again only contains constructors.

Consider the reduction of the Delete term just above:

Delete(Insert(Insert(Insert(EmtpyDB(), 1), 2), 3), 2)

(Insert(Insert(EmtpyDB(), 1), 3)

Delete(Insert(Insert(Insert(EmtpyDB(), 1), 2), 3), 2)

Consider how the match is attempted on the above term with each of the four SetDB equations. The LHSs of the first two equations contain a Find operation. These two equations can be eliminated from consideration immediately, since there is no occurrence of Find anywhere in the subject term (i.e., there are only Delete, Insert, and EmptyDB). The LHS of the last two SetDB equations are possible candidates for a match, since they start with Delete. The third equation cannot match however, since there is no pattern in the subject term that will match.

Delete(EmptyDB(), ...)

We are left with the fourth SetDB equation. This equation does in fact match, as follows:

LHS Subterm	Matched Subject Subterm
Delete	Delete
Insert	outermost application of Insert
s	Insert(Insert(EmptyDB(), 1), 2)
e	3
e'	2

where a subterm is some part of a term. Given this matching, the rule can now be applied, i.e., reduced. The reduction involves systematic substitution of the matched LHS with the appropriate subterms of the RHS of equation 4. The RHS of equation 4 is the following:

if e=e'
then Delete(s, e')
else Insert(Delete(s, e'), e);

e = e'

3 = 2

Insert(Delete(s, e'), e);

Delete(Insert(Insert(Insert(EmptyDB, 1), 2), 3), 2)  =>
    Insert(Delete(Insert(Insert(EmptyDB, 1), 2), 2), 3)

Since the term above still contains a selector operation, it is not yet fully reduced. We therefore apply the same matching process as was used for the first reduction step. As in that case, the first two equations are eliminated immediately as possible matches. The LHS of the third equation also fails to match as before. We again match the fourth equation, this time as follows:

LHS Subterm	Matched Subject Subterm
Delete	Delete
Insert	2nd to the outermost application of Insert
s	Insert(Insert(EmptyDB(), 1), 2)
e	2
e'	2

The difference in this case is that the evaluation of the if predicate in the RHS of equation 4 is now

2 = 2

then Delete(s, e')

Insert(Delete(Insert(Insert(EmptyDB, 1), 2), 1), 2) =>
    Insert(Delete(Insert(EmptyDB(), 1), 2), 3)

1 = 2

    Insert(Delete(Insert(EmptyDB(), 1), 2), 3) =>
        Insert(Insert(Delete(EmptyDB(), 1), 2), 3)

    Insert(Insert(Delete(EmptyDB(), 1), 2), 3) =>
        Insert(Insert(EmptyDB(), 1), 3)

Predicative specification is a complementary form of specification to equational. In the predicative approach, preconditions and postconditions are associated with an operation. The precondition specifies a predicate that must be true before the operation begins. The postcondition specifies a predicate that must be true after the operation completes.

Consider an alternate definition of a set-like database:

object SetDB
    components:  Elem*;
    operations: Insert, Delete, Find, EmptyDB;

    (* Note that we do not need full operation signatures, nor
     * equations, since we are now specifying with pre and post-
     * conditions in place of the equations we used above.
     *)

end SetDB;

obj Elem;

operation Insert
    inputs: d:SetDB, e:Elem;
    outputs: d':SetDB;
    precondition: Find(d, e) = false;
    postcondition: d' = d + e;
end Insert;

operation Find
    inputs: d:SetDB, e:Elem;
    outputs: b:boolean;
    precondition: (* An empty precond means true *) ;
    postcondition: b = e in d;
end Find;

operation Delete
    inputs: d:SetDB, e:Elem;
    outputs: d':SetDB;
    precondition: e in d;
    postcondition: d' = d - e;
end Delete;

operation EmptyDB
    inputs: ;
    outputs: d':SetDB;
    precondition: ;
    postcondition: forall (e:Elem) not Find(d', e);
         (* See discussion below about removing this precond. *)
end EmptyDB;

By definition, failure of a precondition or postcondition is an error. Abstractly this means simply that the operation fails and produces a value of nil. Concretely (e.g., in a system user's manual), this means that the end-user should see some form of appropriate error message.

A specification can be weakened or strengthened by the selective removal or addition of pre and/or post conditions. E.g.,

op Delete is
    in: d:DB, e:Elem;
    out: d':DB;
    precond: Find(d, e) = true;
    postcond: Find(d', e) = false;
end Delete;

op Delete is
    in: d:DB, e:Elem;
    out: d':DB;
    postcond: Find(d', e) = false;
end Delete;

In equational specification, recursion is used to specify a single equation that can be applied in an indefinite (potentially infinite) number of cases. That is, a recursive equation can be applicable to objects from size 1 to an infinite size. The predicative style of specification uses quantification to define predicates that apply to objects of an indefinite size.

Consider the following basic example of universal quantification:

operation FindAllYoungFolks is
    inputs: pdb: PersonDatabase;
    outputs: nl: NameList;
    postcondition:
        forall (p: PersonRecord)
            if (p in pdb) and (p.a < 40)
            then p.n in nl;
    description: (*
        FindAllYoungFolks produces a list of the names of all
        persons in the PersonDatabase whose age is less than 40
    *);
end FindAllYoungFolks;

object PersonDatabase is
    components: PersonRecord*;
    description: (* Same as earlier definitions. *)
end PersonDatabase;

object PersonRecord is
    components: n:Name and a:Age and ad:Address;
    description: (* Same as earlier definitions. *)
end PersonRecord;

object NameList is
    components: Name*;
end NameList;

The following objects and operations further exemplify the use of universal and existential quantification in SpecL. Consider an operation that merges set- like databases, of the type specified earlier:

operation MergeDBs
    inputs: d1:SetDB, d2:SetDB;
    outputs: d3:SetDB;
    postcondition:
        forall (e: Elem)
            if (e in d1) or (e in d2)
            then e in d3;
    description: (*
        The MergeDBs operation merges two databases of the same type
        of element.  The postcondition states that the result of the
        merge is that any element that is in either input d1 or d2
        must be in the output d3.
    *)
end MergeDBs;

The "elsewhere" we look is in the specification of the other DB operations. Specifically, the specifications for SetDB Find and Delete are:

operation Find is
    inputs: d:SetDB, e:Elem;
    outputs: b:boolean;
    precondition: (* An empty precond means true *) ;
    postcondition: b = e in d;
end Find;

operation Delete is
    inputs: d:SetDB, e:Elem;
    outputs: d':SetDB;
    precondition: e in d;
         (* See discussion below about removing this precond. *)
    postcondition: not Find(d,e);
end Delete;

Consider another form of database merge:

object PairedDB is
    components: ElemPair*;
end PairedDB;

object ElemPair is
    components: e1:Elem and e2:Elem;
    description: (* An ElemPair is just a pair of elements. *)
end ElemPair;

operation PairwiseMergeDBs
    inputs: d1:DB, d2:DB;
    outputs: dp: PairedDB
    precond: #d
    postcondition:
        forall (e1,e2: Elem)
            if (e1 in d1) and (e2 in d2)
            then
                exists (ep: ElemPair) (ep in dp) and
                           (ep.e1 = e1) and (ep.e2 = e2)
    description: (*
        PairwiseMergeDBs merges two databases of the same type of
        element into a paired database.  The precondition states
        that the two input DBs must have the same number of
        elements.  The postcondition states that the resulting
        output, dp, must consist of pairs of all the elements that
        are the two input databases.
   *)
end PairwiseMergeDBs

Suppose that only ordered pairs were desired, such that each pair contains the ith element from each of the inputs. This could be specified in a number of ways, including as follows:

operation PairwiseMergeDBs
    ...
    postcondition:
        forall (e1,e2: Elem)
            if (e1 in d1) and (e2 in d2)
            then
                exists (ep: ElemPair) ((ep in dp) and
                PositionOf(ep.e1, d1) = PositionOf(ep.e2, d2))
    ...

function PositionOf(e:Elem, d:DB):(n:number) =
    if d = nil
    then 0
    else if e = d[1]
         then 1
         else PositionOf(e, d[2:#d]) + 1;

The following example shows how a sorted, keyed database can be defined using a combination of equational and predicative specification:

object Elem
    components: k: Key, ElemValue;
    description: (*
        A DB element with an internal key.
    *);
end Elem;

object Key = string;
object ElemValue = ... ;

object SKDB
    components: Elem*;
    operations:
        Insert (SKDB, Elem) -> (SKDB),
        Delete (SKDB, Key) -> (SKDB),
        Find (SKDB, Key) -> (Elem),
        EmptySKDB () -> (SKDB),
        FindNth (SKDB, number) -> (Elem),
        Size (SKDB) -> number,
        SortDB (SKDB, Key) -> (SKDB);
        EmptyDB () -> (SKBD);
    equations:
        var d: SKDB; var e:Elem; var i:number;
        Find(EmptyDB(), k) == EmptyElem;
        Find(Insert(d, e), k') ==
            if e.k=k' then e else find(d, k');
        Delete(EmptyDB(), k) == EmptyDB;
        Delete(Insert(d, k), k') ==
            if k=k'
            then Delete(d, k')
            else Insert(Delete(d, k'), k, e);
        FindNth(EmptyDB(), i) == EmptyElem;
        FindNth(Insert(d,e), i) ==
            if i < 1 then EmptyElem
            else if i = 1 then e
            else FindNth(d,i-1);
        Size(EmptyDB()) == 0;
        Size(Insert(d,e)) == Size(d) + 1;
end SKDB;

operation SortDB
    inputs:    d:SKDB, k:Key;
    outputs:   d':SKDB;
    precondition: ;
    postcondition: if Size(d') > 1 then
                       forall (i:integer | (i >= 1) and (i < Size(d')))
                           FindNth(d',i).k < FindNth(d',i+1).k;
    description: (* Sort a database *);

end SortDB;

operation FindNth
    inputs: d:SKDB, n:number;
    outputs: e:Elem;
    description: (* Find the DB element at position n. *);
end FindNth;

operation Size
    inputs: d:SKDB;
    outputs: i:integer;
    description: (* Compute the size, in elements, of the given DB. *);
end Size;

A negative critique of keyed database specification is that FindNth might best be left invisible to end-users. That is, there may be no reason that users need to find the nth element in a DB. Rather, users simply need the DB sorted, and to be able to find elements by key. Even if this is the case, we still need FindNth in order to fully specify the definition of SortDB.

It was noted earlier that specification is a battle between saying too little and saying too much. In the case of FindNth, the battle has been lost if FindNth is not a necessary user-level operation, since FindNth is still a necessary specification-level function. In the example above, FindNth was specified equationally as a visible operation. The alternate definition as an auxiliary function is the following:

function FindNth(d:SKDB, n:number):(e:Elem) = d[n];

In some cases, it may turn out that what at first appears to be an auxiliary function is in fact a legitimate user-level operation. When this happens, the process of formalizing a specification has helped uncover an incompleteness originally present before the formal definition was considered. In other cases, auxiliary functions should best be left invisible to the user, in which case they remain genuinely auxiliary. In all cases, specifiers must consider carefully when auxiliary functions are necessary.

A noteworthy property of auxiliary functions is that their definitions may be constructive. That is, the body of the function constructs an actual value that the function outputs. Such constructive definitions are in contrast to operations that are defined solely in terms of pre- and post-conditions. A postcondition does not construct a value, but rather states a property that an assumed constructed value must meet.

The astute reader will notice that with the introduction of constructive functions, SpecL has the expressive power of a functional programming language, such as LISP or ML. Hence, using constructive functions, it is possible for specifications to become very much like programs. This is clearly not the intent. Specifiers should always be mindful that the fundamental goal of specification is to define what a system does, not how it works. Constructive auxiliary functions should be used judiciously, so that SpecL specifications remain free of unnecessary program-level detail.

8.5. Inheritance of Formal Specifications

As noted earlier in the manual, part of the rule for inheritance involves inheritance of operations, which in turns involves inheritance of equations and pre/post conditions. The inheritance of operations and equations is straightforward. Viz., all operations and equations of a parent class are inherited by its instances, with systematic name substitution of instance name for parent name.

The inheritance of pre and post conditions warrants further discussion to clarify it fully. Consider the following example.

object GenericDB
    components: GenericRecord*;
    operations:
        AddRecord(GenericDB,GenericRecord)->GenericDB;
        DelRecord(GenericDB,GenericKey)->GenericDB;
        UpdateRecord(GenericDB,GenericRecord)->GenericDB;
        FindRecord(GenericDB,GenericKey)->GenericRecord;
    description: (*
        A GenericDB is the parent for more specific databases, which will
        contain more specific forms of records.
    *);
end GenericDB;

object GenericRecord
    components: key:GenericKey;
    description: (*
        A generic record contains only a key field, which will be common to all
        instances.  The key is used to access the record in a GenericDB.
    *);
end GenericRecord;

object GenericKey
    description: (*
        A generic key is componentless, to be specialized further by its
        instances.
    *);
end GenericKey;

object PersonDB extends GenericDB
    where:
        GenericRecord = PersonRecord;
        GenericKey = PersonId;
    description: (*
        A PersonDB is a specialization of GenericDB.  Note use of the where
        attribute, which means that UserRecord replaces all occurrences of
        GenericRecord in the defintion of GenericDB, and PersonId replaces all
        occurences of GenericKey.
    *);
end UserDB;

object PersonRecord extends GenericRecord
    components: name:Name and address:Address and age:Age and Sex;
    description: (*
        A PersonRecord specializes a GenericRecord by adding appropriate
        components for Name, etc.
    *);
end UserRecord;

object PersonId extends GenericKey = number
    description: (*
        A PersonId specializes GenericKey to be a number.  In so doing, the
        access key for a PersonRecord can be some unique numeric id, such as
        social security number, for example.
    *);
end PersonId;
op AddRecord(gdb:GenericDB, gr:GenericRecord)->(gdb':GenericDB)
    pre: FindRecord(gdb, gr.key) = nil;
    post: gdb' = gdb + gr;
end;

op DelRecord(gdb:GenericDB, key:GenericKey)->(gdb':GenericDB)
    pre: FindRecord(gdb, key) != nil;
    post: gdb' = gdb - FindRecord(gdb, key);
end;

op UpdateRecord(gdb:GenericDB, gr:GenericRecord)->(gdb':GenericDB)
    pre: FindRecord(gdb, gr.key) != nil;
    post: gdb' = gdb - FindRecord(gdb, gr.key) + gr;
end;

op FindRecord(gdb:GenericDB, key:GenericKey)->(gr':GenericRecord)
    pre: ;
    post: (gr' in gdb) and (gr'.key = key);
end;

op AddRecord(gdb:PersonDB, gr:PersonRecord)->(gdb':PersonDB)
    pre: FindRecord(gdb, gr.key) = nil;
    post: gdb' = gdb + gr;
end;

op DelRecord(gdb:PersonDB, key:PersonId)->(gdb':PersonDB)
    pre: FindRecord(gdb, key) != nil;
    post: gdb' = gdb - FindRecord(gdb, key);
end;

op UpdateRecord(gdb:PersonDB, gr:PersonRecord)->(gdb':PersonDB)
    pre: FindRecord(gdb, gr.key) != nil;
    post: gdb' = gdb - FindRecord(gr.key) + gr;
end;

op FindRecord(gdb:PersonDB, key:PersonId)->(gr':PersonRecord)
    pre: ;
    post: (gr' in gdb) and (gr'.key = key);
end;

op AddRecord(gdb:PersonDB, gr:PersonRecord)->(gdb':PersonDB)
    pre: #gr.name <= 30 and #gr.address <= 50 and
             gr.age >= 0 and gr.age <= 200;
end;

op AddRecord(gdb:PersonDB, gr:PersonRecord)->(gdb':PersonDB)
    pre: (FindRecord(gdb, gr.key) = nil) and
             (#(gr.name) <= 30) and (#(gr.address) <= 50) and
                 (gr.age >= 0) and (gr.age <= 200);
    post: gdb' = gdb + gr;
end;