Object-oriented rules

The behavior associated with messages is specified by rewrite rules in a declarative way. For example, the semantics of the credit, debit, and from_to_transfer_ messages declared in Section 15.1.2 may be given as follows:

  vars A B : Oid .
  var  M : Nat .
  vars N N' : Int .

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

  crl [debit] :
    debit(A, M)
    < A : Account | bal : N >
    => < A : Account | bal : N - M >
    if N >= M .

  crl [transfer] :
    (from A to B transfer M)
    < A : Account | bal : N >
    < B : Account | bal : N' >
    => < A : Account | bal : N - M >
       < B : Account | bal : N' + M >
    if N >= M .

Note that the multiset structure of the configuration provides the top-level distributed structure of the system and allows concurrent application of the rules. The reader is referred to [58] for a detailed explanation of the logical semantics of the object-oriented model of computation supported by Maude.

In object-oriented modules it is possible not to mention in a given rule those attributes of an object that are not relevant for that rule. The attributes mentioned only on the lefthand side of a rule are preserved unchanged, the original values of attributes mentioned only on the righthand side do not matter, and all attributes not explicitly mentioned are left unchanged (see Section 15.8 for more details). For instance, a message for changing the age of a person defined by the class Person (introduced in Section 15.1.2) may be defined as follows:

  msg to_:`new`age_ : Oid Nat -> Msg .
  var A : Nat .
  var O : Oid .

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

The attributes name and account, which are not mentioned in this rule, are not changed when applying the rule. The value of the age attribute is replaced by the given new age, independently of its previous value.

The following module ACCOUNT contains all the declarations above defining the class Account. Note that Qid is declared as a subsort of Oid, making any quoted identifier a valid object identifier.

 (omod ACCOUNT is
    protecting QID .
    protecting INT .

    subsort Qid < Oid .
    class Account | bal : Int .
    msgs credit debit : Oid Int -> Msg .
    msg from_to_transfer_ : Oid Oid Int -> Msg .

    vars A B : Oid .
    var  M : Nat .
    vars N N' : Int .

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

    crl [debit] :
      debit(A, M)
      < A : Account | bal : N >
      => < A : Account | bal : N - M >
      if N >= M .

    crl [transfer] :
      (from A to B transfer M)
      < A : Account | bal : N >
      < B : Account | bal : N' >
      => < A : Account | bal : N - M >
         < B : Account | bal : N' + M >
      if N >= M .
  endom)

We can now rewrite a simple configuration consisting of an account and a message as follows:

  Maude> (rew < 'A-06238 : Account | bal : 2000 >
              debit('A-06238, 1000) .)

  result Object : 
    < 'A-06238 : Account | bal : 1000 >

The following module contains the declarations for the class SavingAccount.

 (omod SAVING-ACCOUNT is
    including ACCOUNT .
    protecting FLOAT .
    class SavingAccount | rate : Float .
    subclass SavingAccount < Account .
  endom)

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-time^15.2attribute in account objects.

We can now rewrite a configuration, obtaining the following result.

  Maude> (rew < 'A-73728 : SavingAccount | bal : 5000, rate : 3.0 >
              < 'A-06238 : Account | bal : 2000 >
              < 'A-28381 : SavingAccount | bal : 9000, rate : 3.0 >
              debit('A-06238, 1000)
              credit('A-73728, 1300)
              credit('A-28381, 200) .)

  result Configuration :
              < 'A-06238 : Account | bal : 1000 >
              < 'A-73728 : SavingAccount | bal : 6300, rate : 3.0 >
              < 'A-28381 : SavingAccount | bal : 9200, rate : 3.0 >

We can also search over configurations. In this case the search pattern takes into account object-oriented information, finding also states where a subclass matches the pattern. For example, we can look for final states having accounts with balance less than $8000$ with the following command:

  Maude> (search in SAVING-ACCOUNT :
              < 'A-73728 : SavingAccount | bal : 5000, rate : 3.0 >
              < 'A-06238 : Account | bal : 2000 >
              < 'A-28381 : SavingAccount | bal : 9000, rate : 3.0 >
              debit('A-06238, 1000)
              credit('A-73728, 1300)
              credit('A-28381, 200)
           =>! C:Configuration 
               < O:Oid : Account | bal : N:Nat > 
           such that N:Nat < 8000 .)
  search in SAVING-ACCOUNT : 
    < 'A-73728 : SavingAccount | bal : 5000, rate : 3.0 >
    < 'A-06238 : Account | bal : 2000 > 
    < 'A-28381 : SavingAccount | bal : 9000, rate : 3.0 > 
    debit('A-06238, 1000)
    credit('A-73728, 1300)
    credit('A-28381, 200) 
    =>! C:Configuration 
        < O:Oid : V#0:Account | bal : N:Nat, V#1:AttributeSet > .
           
  Solution 1
  C:Configuration --> 
    < 'A-28381 : SavingAccount | bal : 9200,rate : 3.0 > 
    < 'A-73728 : SavingAccount | bal : 6300,rate : 3.0 > ; 
  N:Nat --> 1000 ; 
  O:Oid --> 'A-06238 ; 
  V#0:Account --> Account ; 
  V#1:AttributeSet --> (none).AttributeSet

  Solution 2
  C:Configuration --> 
    < 'A-06238 : Account | bal : 1000 > 
    < 'A-28381 : SavingAccount | bal : 9200, rate : 3.0 > ; 
  N:Nat --> 6300 ; 
  O:Oid --> 'A-73728 ; 
  V#0:Account --> SavingAccount ; 
  V#1:AttributeSet --> rate : 3.0

  No more solutions.

Notice that the search pattern has been transformed so that objects in subclasses match. In this example, we obtain as solutions both an object of class Account and an object in the subclass SavingAccount.