Module instantiation

We show in this section how, by instantiating the object-oriented module OO-STACK2 given in Section 15.3.3, we can obtain a specification of a stack of banking accounts. We first specify a view Account from the object-oriented theory CELL (in Section 15.3.1) to the object-oriented module ACCOUNT (in Section 15.1.4).

 (view Account from CELL to ACCOUNT is
    sort Elt to Int .
    class Cell to Account .
    attr Cell . contents to bal .
  endv)

Now we can do the following rewriting on the module resulting from the instantiation.

  Maude> (rew in OO-STACK2{Account} 
                   * (class Account to Account,
                      class Stack{Account} to Stack{Account},
                      class Node{Account} to Node{Account},
                      attr Stack{Account} . first to head,
                      attr Account . bal to balance,
                      msg _elt_ to element,
                      sort Int to Integer) :
  < 'stack : Stack{Account} | head : null >
  < 'A-73728 : Account | balance : 5000 >
  < 'A-06238 : Account | balance : 2000 >
  < 'A-28381 : Account | balance : 15000 >
  ('stack push 'A-73728)
  ('stack push 'A-06238)
  ('stack push 'A-28381)
  ('stack top 'A-06238)
  ('stack pop) .)

  result Configuration :
    element('A-28381,15000)
    < 'A-06238 : Account | balance : 2000 >
    < 'A-28381 : Account | balance : 15000 >
    < 'A-73728 : Account | balance : 5000 >
    < 'stack : Stack{Account}| head : o('stack, 1)>
    < o('stack, 0) : Node{Account} | next : null, node : 'A-06238 >
    < o('stack, 1) : Node{Account} | 
        next : o('stack, 0), node : 'A-73728 >