Up Next
Go up to 3.2 Object-Oriented Modules
Go forward to 3.2.2 Transforming Object-Oriented Modules into System Modules

3.2.1 The Syntax of Object-Oriented Modules

Classes are defined with the keyword class, followed by the name of the class C, and by a list of attribute declarations separated by commas. Each attribute declaration has the form a : S, where a is an attribute identifier and S is the sort in which the values of the attribute identifier range. That is, class declarations have the form class C | a_1 : S_1 , ..., a_n : S_n . We can declare classes without attributes using syntax class C .

The basic syntax for class declarations is given by the following operators and subsort relationship. 

    subsort AttrDecl < AttrDeclList .
    op _:_ : Token Sort -> AttrDecl [prec 40] .
    op _,_ : AttrDeclList AttrDeclList -> AttrDeclList [assoc] .

    op class_|_. : Sort AttrDeclList -> ClassDecl .
    op class_. : Sort -> ClassDecl .

In this example, the only attribute of an account is its bal(ance), which is declared to be a value in MachineInt, a sort declared in the module MACHINE-INT. The three kinds of messages involving accounts are credit, debit, and transfer messages, whose user-definable syntax is introduced by the keyword msg. Notice the use of msgs to define multiple messages with the same arity in a single declaration.

The syntax for message declarations is given by the following operators. 

    op msg_:_->_. : Token SortList Sort -> MsgDecl .
    op msgs_:_->_. : NeTokenList SortList Sort -> MsgDecl .

The rewrite rules in the module specify in a declarative way the behavior associated with the messages. The multiset structure of the configuration provides the top-level distributed structure of the system and allows concurrent application of the rules [38]. For example, we can rewrite a simple configuration consisting of an account and a message as follows. 

  Maude> (rew < 'Peter : Accnt | bal : 2000 > 
              debit('Peter, 1000) .)
  
  Result Object : < 'Peter : Accnt | bal : 1000 >

Class inheritance is directly supported by Maude's order-sorted type structure. A subclass declaration C < C' in an object-oriented module is just a particular case of a subsort declaration C < C'. The effect of a subclass declaration is that the attributes, messages, and rules of all the superclasses as well as the newly defined attributes, messages, and rules of the subclass characterize the structure and behavior of the objects in the subclass.

For example, we can define an object-oriented module SAV-ACCNT of saving accounts introducing a subclass SavAccnt of Accnt with a new attribute rate recording the interest rate of the account. We leave unspecified the rules for computing and crediting the interest of an account according to its rate whose proper expression should introduce a real-time29 attribute in account objects. 

  (omod SAV-ACCNT is
    including ACCNT .
    class SavAccnt | rate : MachineInt .
    subclass SavAccnt < Accnt .
   endom)

In this example, there is only one class immediately above SavAccnt, namely, Accnt. In general, however, a class C may be defined as a subclass of several classes D1,...,Dk, i.e., multiple inheritance is supported. If an attribute and its sort have already been declared in a superclass, they should not be declared again in the subclass. Indeed, all such attributes are inherited. In the case of multiple inheritance, the only requirement that is made is that if an attribute occurs in two different superclasses, then the sort attributed to it in each of those superclasses must be the same. In summary, a class inherits all the attributes, messages, and rules from all its superclasses. An object in the subclass behaves exactly as any object in any of the superclasses, but it may exhibit additional behavior due to the introduction of new attributes, messages, and rules in the subclass.

As for subsort relationships, we can declare multiple subclass relationships in the same declaration. Thus, given, for example, classes A, ..., H, we can have a declaration such as 

    subclasses A B C < D E < F G H .
Since class names have the same form as sorts, in the signature used to parse Full Maude given in Appendix C, we use the sort Sort to parse them, and the sort SortList for lists of names of classes. The syntax for subclass declarations is given by the following operators. 
    op subclass_. : SubsortRel -> SubclassDecl .
    op subclasses_. : SubsortRel -> SubclassDecl .

Objects in the class SavAccnt will have an attribute bal and can receive messages debiting, crediting and transferring funds exactly as any other object in the class Accnt. We can now rewrite a configuration, obtaining the following result. 

  Maude> (rew < 'Paul : SavAccnt | bal : 5000, rate : 3 >
              < 'Peter : Accnt | bal : 2000 >
              < 'Mary : SavAccnt | bal : 9000, rate : 3 >
              debit('Peter, 1000)
              credit('Paul, 1300)
              credit('Mary, 200) .)

  Result Configuration : 
              < 'Peter : Accnt | bal : 1000 > 
              < 'Paul : SavAccnt | bal : 6300 , rate : 3 > 
              < 'Mary : SavAccnt | bal : 9200 , rate : 3 >

The top level syntax for object-oriented modules is given by the following declarations. 

  subsorts SDeclList MsgDecl SubclassDecl ClassDecl < ODeclList .

  op omod_is_endom : ModuleName ODeclList -> PreModule .
Up Next