Parameterized object-oriented modules

Like any other type of module, object-oriented modules can be parameterized, and, like sort names, class names may also be parameterized. The naming of parameterized classes follows the same conventions discussed in Section 6.3.3 for parameterized sorts.

As an example of an object-oriented parameterized module, we define a stack of elements. We define a class Stack{X} as a linked sequence of node objects. Objects of class Stack{X} have a single attribute first, containing the identifier of the first node in the stack. If the stack is empty, the value of the first attribute is null. Each object of class Node{X} has an attribute next holding the identifier of the next node--which should be null if there is no next node--and an attribute contents to store a value of sort X$Elt. Notice that node identifiers are of the form $\texttt{o(}S\texttt{,}N\texttt{)}$, where $S$ is the identifier of the stack object to which the node belongs, and $N$ is a natural number. The messages push, pop and top have as their first argument the identifier of the object to which they are addressed, and will cause, respectively, the insertion at the top of the stack of a new element, the removal of the top element, and the sending of a response message elt containing the element at the top of the stack to the object making the request.

 (omod OO-STACK{X :: TRIV} is
    protecting INT .
    protecting QID .
    subsort Qid < Oid .
    class Node{X} | next : Oid, contents : X$Elt .
    class Stack{X} | first : Oid .
    msg _push_ : Oid X$Elt -> Msg .
    msg _pop : Oid -> Msg .
    msg _top_ : Oid Oid -> Msg .
    msg _elt_ : Oid X$Elt -> Msg .

    op null : -> Oid .
    op o : Oid Int -> Oid .

    vars O O' O'' : Oid .
    var  E : X$Elt .
    var  N : Int .

    rl [top] : *** top on a non-empty stack
       < O : Stack{X} | first : O' >
       < O' : Node{X} | contents : E >
       (O top O'')
       => < O : Stack{X} | >
          < O' : Node{X} | >
          (O'' elt E) .

    rl [push1] : *** push on a non-empty stack
       < O : Stack{X} | first : o(O, N) >
       (O push E)
       => < O : Stack{X} | first : o(O, N + 1) >
          < o(O, N + 1) : Node{X} |
                contents : E, next : o(O, N) > .

    rl [push2] : *** push on an empty stack
       < O : Stack{X} | first : null >
       (O push E)
       => < O : Stack{X} | first : o(O, 0) >
          < o(O, 0) : Node{X} | contents : E, next : null > .

    rl [pop] : *** pop on a non-empty stack
       < O : Stack{X} | first : O' >
       < O' : Node{X} | next : O'' >
       (O pop)
       => < O : Stack{X} | first : O'' > .
  endom)

Notice that top and pop messages are not received if the stack is empty.

We may want to define stacks storing not just data elements of a particular sort, but actually objects in a particular class. We can define an object-oriented module with the intended behavior as the parameterized module OO-STACK2 below, which is parameterized by the object-oriented theory CELL introduced in Section 15.3.1. Notice that the main difference with respect to the previous STACK version is in the attribute node, that keeps the identifier of the object where the contents can be found instead of the attribute contents that provided direct access to those contents.

 (omod OO-STACK2{X :: CELL} is
    protecting INT .
    protecting QID .
    subsort Qid < Oid .
    class Node{X} | next : Oid, node : Oid .
    class Stack{X} | first : Oid .
    msg _push_ : Oid Oid -> Msg .
    msg _pop : Oid -> Msg .
    msg _top_ : Oid Oid -> Msg .
    msg _elt_ : Oid X$Elt -> Msg .

    op null : -> Oid .
    op o : Oid Int -> Oid .

    vars O O' O'' O''' : Oid .
    var  E : X$Elt .
    var  N : Int .

    rl [top] : *** top on a non-empty stack
       < O : Stack{X} | first : O' >
       < O' : Node{X} | node : O'' >
       < O'' : X$Cell | contents : E >
       (O top O''')
       => < O : Stack{X} | >
          < O' : Node{X} | >
          < O'' : X$Cell | >
          (O''' elt E) .

    rl [push1] : *** push on a non-empty stack
       < O : Stack{X} | first : o(O, N) >
       (O push O')
       => < O : Stack{X} | first : o(O, N + 1) >
          < o(O, N + 1) : Node{X} |
                 next : o(O, N), node : O' > .

    rl [push2] : *** push on an empty stack
       < O : Stack{X} | first : null >
       (O push O')
       => < O : Stack{X} | first : o(O, 0) >
          < o(O, 0) : Node{X} | next : null, node : O' > .

    rl [pop] : *** pop on a non-empty stack
       < O : Stack{X} | first : O' >
       < O' : Node{X} | next : O'' >
       (O pop)
       => < O : Stack{X} | first : O'' > .
  endom)