From object-oriented modules to system modules

The best way to understand classes and class inheritance in Full Maude is by making explicit the full structure of an object-oriented module, which is left somewhat implicit by the syntactic conventions adopted for them. Indeed, although object-oriented modules provide convenient syntax for programming object-oriented systems, their semantics can be reduced to that of system modules. We can regard the special syntax reserved for object-oriented modules as syntactic sugar. In fact, each object-oriented module can be translated into a corresponding system module whose semantics is by definition that of the original object-oriented module.

In the translation process, the most basic structure shared by all object-oriented modules is made explicit by the CONFIGURATION functional module. The translation of a given object-oriented module extends this structure with the classes, messages and rules introduced by the module. For example, the following system module is the translation of the ACCOUNT module introduced earlier. Note that a subsort Account of Cid is introduced. The purpose of this subsort is to range over the class identifiers of the subclasses of Account. For the moment, no such subclasses have been introduced; therefore, at present the only constant of sort Account is the class identifier Account.

  mod ACCOUNT is
    protecting INT .
    protecting QID .
    including CONFIGURATION+ .
    including CONFIGURATION .
    sorts Account .
    subsort Qid < Oid .
    subsort Account < Cid .
    op Account : -> Account .
    op credit : Oid Int -> Msg [msg] .
    op debit : Oid Int -> Msg [msg] .
    op from_to_transfer_ : Oid Oid Int -> Msg [msg] .
    op bal :_ : Int -> Attribute .
    var A : Oid .
    var B : Oid .
    var M : Int .
    var N : Int .
    var N' : Int .
    var V@Account : Account .
    var ATTS@0 : AttributeSet .
    var V@Account1 : Account .
    var ATTS@2 : AttributeSet .
    rl [credit] :
      credit(A, M)
      < A : V@Account | bal : N, ATTS@0 >
      => < A : V@Account | bal : (N + M), ATTS@0 > .
    crl [debit] :
      debit(A, M)
      < A : V@Account | bal : N, ATTS@0 >
      => < A : V@Account | bal : (N - M), ATTS@0 >
      if N >= M = true .
    crl [transfer] :
      (from A to B transfer M)
      < A : V@Account | bal : N, ATTS@0 >
      < B : V@Account1 | bal : N', ATTS@2 >
      => < A : V@Account | bal : (N - M), ATTS@0 >
         < B : V@Account1 | bal : (N' + M), ATTS@2 >
      if N >= M = true .
  endm

We can describe the desired transformation from an object-oriented module to a system module as follows:^15.5

• The module CONFIGURATION+ is imported, which in turn imports the module CONFIGURATION from Section 8.1. It adds a function class which returns the actual class of the given object, and also syntax for objects with no attributes <_:_| >.

    mod CONFIGURATION+ is
      protecting CONFIGURATION .
      op <_:_| > : Oid Cid -> Object .
      op class : Object -> Cid .
      eq < O:Oid : C:Cid | > = < O:Oid : C:Cid | none > .
      eq class(< O:Oid : C:Cid | A >) = C:Cid .
    endm
  

• For each class declaration of the form $\texttt{class }C\texttt{ \vert } a_1\texttt{:} S_1\texttt{,} \ldots\texttt{,} a_n\texttt{:} S_n$, the following is introduced: a subsort $C$ of sort Cid, a constant $C$ of sort $C$, and declarations of operations
  
  $$a_i \texttt{ :\_} \texttt{ : } S_i \texttt{ -> Attribute}$$
  
  
  for each attribute $a_i$.
• For each subclass relation $C$ < $D$ a subsort declaration
    subsort C < D .
  

  is introduced, and the set of attributes for objects of class $C$ is completed with those of $D$.

• The system modules resulting from the transformation have the special features supported in Core Maude for object-based programming explained in Chapter 8. Specifically, the msg attribute is added to message declarations starting with the msg keyword.
• The rewrite rules are modified to make them applicable to all objects of the given classes and of their subclasses, that is, not only to objects whose class identifiers are those explicitly given. The rules are then ``inherited'' by all objects in their subclasses by replacing the class identifiers in the objects in the rules by variables of the corresponding class sort. Variables of sort AttributeSet are also introduced, to range over the additional attributes that may appear in objects of a subclass. That is, each object expression $\texttt{ < }O\texttt{ : }C\texttt{ \vert }\ldots\texttt{\ > }$ appearing in a rule is translated into $\texttt{ <\ }O\texttt{ : }X\texttt{ \vert } \ldots \texttt{, }Atts\texttt{ >}$, where the new variable $X$ is declared of sort $C$, and the new variable $Atts$ has sort AttributeSet.
• The rewrite rules are modified to give the user the possibility of not mentioning in a given rule those attributes of an object that are not relevant for that rule. To explain the transformation, let $\overrightarrow{a:v}$ denote the attribute-value pairs $a_{1}:v_{1},\ldots,a_{n}:v_{n}$, where $\overrightarrow{a}$ are the attribute identifiers of a given class $C$ (after completing it with all the attributes in its superclasses) having $\overrightarrow{S}$ as the corresponding sorts of values prescribed for those attributes. Then, in object-oriented modules we allow rules where the attributes for an object $O$, mentioned in the lefthand and righthand sides of a rule, need not exhaust all the object's attributes, but can instead be in any of two arbitrary subsets of the object's attributes. We can picture this as follows
  
  $$\ldots \langle O : C \mid \overrightarrow{al:vl}, \overrighta... ...\overrightarrow{ab:vb'}, \overrightarrow{ar:vr} \rangle \ldots$$
  
  
  where $\overrightarrow{al}$ are the attributes appearing only on the left, $\overrightarrow{ab}$ are the attributes appearing on both sides, and $\overrightarrow{ar}$ are the attributes appearing only on the right. In the transformation into a system module, this rule is translated into
  $$\begin{eqnarray*} && \ldots \langle O : X \mid \overrightarrow{al:vl}, \overri... ...ghtarrow{ar:vr}, \overrightarrow{ac:x'}, Atts\/ \rangle \ldots \end{eqnarray*}$$
  
  
  where $X$ is a variable of sort $C$, $\overrightarrow{ac}$ are the attributes defined in the class $C$ that do not appear in $\overrightarrow{al}$, $\overrightarrow{ab}$, or $\overrightarrow{ar}$, the $\overrightarrow{x}$ and $\overrightarrow{x'}$ are new variables of the appropriate sorts, and $Atts$ matches the remaining attribute-value pairs.

The rewrite rules given in the original ACCOUNT module are interpreted here--according to the conventions already explained--in a form that can be inherited by subclasses of Account that could be defined later. Thus, SavingAccount inherits the rewrite rules for crediting and debiting accounts, and for transferring funds between accounts that had been defined for Account.

Let us illustrate the treatment of class inheritance with the system module resulting from the transformation of the module SAVING-ACCOUNT introduced previously.

  mod SAVING-ACCOUNT is
    including CONFIGURATION+ .
    including CONFIGURATION .
    including ACCOUNT .
    sorts SavingAccount .
    subsort SavingAccount < Cid .
    subsort SavingAccount < Account .
    op SavingAccount : -> SavingAccount .
    op rate :_ : Int -> Attribute .
  endm

Note that by translating a rule like credit above

  rl [credit] :
    credit(A, M)
    < A : Account | bal : N >
    => < A : Account | bal : (N + M) > .

into its corresponding transformed form

  rl [credit] :
    credit(A, M)
    < A : V0@:Account | bal : N, V1@:AttributeSet >
    => < A : V0@:Account | bal : (N + M), V1@:AttributeSet > .

it is guaranteed that the rule will be applicable to objects of class Account as well as of any of its subclasses.

Note also that a rule like change-age (discussed in Section 15.1.4)

  rl [change-age] :
    < O : Person | >
    to O : new age A
    => < O : Person | age : A > .

is translated into a rule like

  rl [change-age] :
    < O : V0@:Person | name : V1:String, age : V2:Nat,
                       account : V3:Oid, V4@:AttributeSet >
    to O : new age A
    => < O : V0@:Person | age : A, name : V1:String,
                          account : V3:Oid, V4@:AttributeSet > .

With this translation we allow the rule to be applied to objects in subclasses of Person. Furthermore, we guarantee that it is only applied to well-formed objects, that is, to objects with all the required attributes.

See [27] for a detailed explanation of the transformation of object-oriented modules into system modules and how their semantics is by definition that of the original object-oriented module.