3.2.2 Transforming Object-Oriented Modules into System Modules

The best way to understand classes and class inheritance in Maude is by making explicit the full structure of an object-oriented module, which is left somewhat implicit in the syntactic conventions adopted for them. Indeed, although Maude's 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.

However, although Maude's object-oriented modules can in this way be reduced to system modules, there are of course important conceptual advantages provided by the syntax of object-oriented modules, because it allows the user to think and express his or her thoughts in object-oriented terms whenever such a viewpoint seems best suited for the problem at hand. Those conceptual advantages would be lost if only system modules were provided.

In the translation process, the most basic structure shared by all object-oriented modules is made explicit by the CONFIGURATION functional module defined at the beginning of this section. 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 ACCNT module introduced earlier. Note that a subsort Accnt of Cid is introduced. The purpose of this subsort is to range over the class identifiers of the subclasses of Accnt. For the moment, no such subclasses have been introduced; therefore, at present the only constant of sort Accnt is the class identifier Accnt.

  mod ACCNT is 
        including MACHINE-INT . 
        including QID . 
        including CONFIGURATION .
        sorts Accnt . 
        subsort Qid < Oid . 
        subsort Accnt < Cid . 
        op Accnt : -> Accnt . 
        op credit : Oid MachineInt -> Msg . 
        op debit : Oid MachineInt -> Msg . 
        op transfer_from_to_ : MachineInt Oid Oid -> Msg . 
        op bal :_ : MachineInt -> Attribute . 
        var A : Oid . 
        var B : Oid . 
        var M : MachineInt . 
        var N : MachineInt . 
        var N' : MachineInt . 
        var V@Accnt : Accnt . 
        var ATTS@0 : AttributeSet . 
        var V@Accnt1 : Accnt . 
        var ATTS@2 : AttributeSet . 
        rl [credit] : credit(A, M) 
                < A : V@Accnt | bal : N, none, ATTS@0 > 
          => < A : V@Accnt | bal : (N + M), ATTS@0 > . 
        crl [debit] : debit(A, M)
                < A : V@Accnt | bal : N, none, ATTS@0 > 
          => < A : V@Accnt | bal : (N - M), ATTS@0 > 
             if N > M = true . 
        crl [transfer] : (transfer M from A to B) 
                < A : V@Accnt | bal : N, none, ATTS@0 > 
                < B : V@Accnt1 | bal : N', none, ATTS@2 > 
          => < A : V@Accnt | bal : (N - M), ATTS@0 > 
             < B : V@Accnt1 | 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³⁰:

• The module CONFIGURATION is imported.
• For each class declaration of the form class C | a₁: S₁, ..., a_n: S_n, the following has to be introduced: a subsort C of sort Cid, a constant C of sort C, and declarations of operations a_i :_ : S_i -> Attribute for each attribute a_i.
• For each subclass relation C < C' a subsort declaration subsort C < C' . is introduced, and the set of attributes for objects of class C are completed with those of C'.
• 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 < O : C | ... > appearing in a rule, is translated into < O : X | ..., Atts > where the new variable X is declared of sort C, and the new variable Atts has sort AttributeSet.
• As described in [38], we simplify the notation used in object-oriented modules by giving 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 this convention, let  |¯a:v¯|  denote the attribute-value pairs a₁:v₁,...,a_n:v_n, where the  |¯a¯|  are the attribute identifiers of a given class C (after completing it with all the attributes in its superclasses) having  |¯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 two arbitrary subsets of the object's attributes. We can picture this as follows ...<O : C |  |¯al:vl¯| ,  |¯ab:vb¯|  >... --> ...<O : C |  |¯ab:vb'¯| ,  |¯ar:vr¯|  >... where  |¯al¯|  are the attributes appearing only on the left,  |¯ab¯|  are the attributes appearing on both sides, and  |¯ar¯|  are the attributes appearing only on the right. In the transformation into a system module, this rule is translated into

  		...<O : X |  |¯al:vl¯| ,  |¯ab:vb¯| ,  |¯ar:x¯| ,  |¯ac:x'¯| , Atts >...
  		--> ...<O : X |  |¯al:vl¯| ,  |¯ab:vb'¯| ,  |¯ar:vr¯| ,  |¯ac:x'¯| , Atts >...

  where X is a variable of sort C,  |¯ac¯|  are the attributes defined in the class C that do not appear in  |¯al¯| ,  |¯ab¯| , or  |¯ar¯| , the  |¯x¯|  and  |¯x'¯|  are new variables of the appropriate sorts, and Atts matches the remaining attribute-value pairs. Although the form of the rule obtained is slightly different from the one given in [38], the convention is similar to the convention presented there: The attributes mentioned only on the left are preserved unchanged, the original values of attributes mentioned only on the right do not matter, and all attributes not explicitly mentioned are left unchanged.

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

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

  mod SAV-ACCNT is 
    including CONFIGURATION .
    including ACCNT .
    sorts SavAccnt . 
    subsort SavAccnt < Cid . 
    subsort SavAccnt < Accnt . 
    op SavAccnt : -> SavAccnt . 
    op rate :_ : MachineInt -> Attribute . 
  endm