Chapter 6
Object-Oriented Modules

Distributed systems can be naturally modeled in Maude as multisets of entities, loosely coupled by some suitable communication mechanism. An important example is object-based distributed systems in which the entities are objects, each with a unique identity, and the communication mechanism is message passing.

Concurrent object-oriented systems can be defined by means of object-oriented modules—introduced by the keyword omod...endom—with a syntax that assumes acquaintance with the basic object-oriented entities, such as objects, messages and configurations, and supports linguistic distinctions appropriate for the object-oriented case.

As we will see in Section 6.4, we may have specifications of object-based systems in system modules. However, although Maude’s system modules are sufficient for specifying object-oriented systems, there are important conceptual advantages provided by the syntax for object-oriented modules. Such syntax allows the user to think and express his/her thoughts in object-oriented terms whenever such a viewpoint seems best suited for the problem at hand. Those conceptual advantages would be partially lost if only system modules were provided.

Object-oriented modules are however just syntactic sugar: they are internally transformed into system modules for execution purposes (see Section 6.5). All object-oriented modules implicitly include the CONFIGURATION module (see Section 6.1), and thus assume the syntax it provides. The module CONFIGURATION defines the basic concepts of concurrent object systems; among others, and besides the Configuration sort, it includes the declarations of sorts Oid of object identifiers, Cid of class identifiers, Object for objects, and Msg for messages.

6.1 Objects, messages and configurations

Maude supports the modeling of object-based systems by providing a predefined CONFIGURATION module. This module declares sorts representing the essential concepts of object, message, and configuration, along with a notation for object syntax that serves as a common language for specifying object-based systems. In addition, there is an object-message fair rewriting strategy that is well suited for executing object system configurations (see Section 6.3). Object-oriented modules will implicitly import the CONFIGURATION module, and use its definitions to build object-oriented systems. Indeed, as we will explain in Section 6.5, Maude desugars object-oriented modules into system modules, built on the CONFIGURATION module as any user can directly do.

The predefined module CONFIGURATION in the file prelude.maude provides sorts and constructors for modeling object-based systems.

mod CONFIGURATION is 
 sorts Attribute AttributeSet . 
 subsort Attribute < AttributeSet . 
 op none : -> AttributeSet [ctor] . 
 op _,_ : AttributeSet AttributeSet -> AttributeSet 
   [ctor assoc comm id: none format (d d s d)] . 
 
 sorts Oid Cid Object Msg Portal Configuration . 
 subsort Object Msg Portal < Configuration . 
 op <_:_|_> : Oid Cid AttributeSet -> Object 
   [ctor object 
    special (id-hook ObjectConstructorSymbol 
      op-hook attributeSetSymbol (_,_ : AttributeSet AttributeSet ~> AttributeSet))] . 
 op none : -> Configuration [ctor] . 
 op __ : Configuration Configuration -> Configuration 
   [ctor config assoc comm id: none] . 
 op <> : -> Portal [ctor portal] . 
 
 op getClass : Object -> Cid . 
 eq getClass(< O:Oid : C:Cid | A:AttributeSet >) = C:Cid . 
endm
     

The basic sorts needed to describe an object system are: Object, Msg (messages), and Configuration. For the different elements involved in their construction, four additional sorts are declared: Oid (object identifiers), Cid (class identifiers), Attribute (a named element of an object’s state), and AttributeSet (multisets of attributes).

An object in a given state is represented as a term of the form

< O : C | $⟨$att-1$⟩$, ..., $⟨$att-n$⟩$ >
     

< O : C | a1 : v1, ..., an : vn >
     

< O : C | >
     

or

< O : C | none >
     

Messages do not have a fixed syntactic form; their syntax is instead defined by the user for each application. The only assumption made by the system is that the first argument of a message is the identifier of its destination object. This requirement is key for the correct operation of the object-message fair rewriting strategy (see Section 6.3).

The concurrent state of an object-oriented system is then a multiset of objects and messages, of sort Configuration, with multiset union described with empty syntax __, and with assoc, comm, and id: none as operator attributes. The empty configuration is represented by the constant none. The attribute config declares that configurations constructed with __ support the special object-message fair rewriting behavior (see Section 6.3).

A typical configuration will have the form

$⟨$Ob-1$⟩$ ... $⟨$Ob-k$⟩$  $⟨$Mes-1$⟩$ ... $⟨$Mes-n$⟩$
     

An important consideration about object systems is that object names must be unique. More precisely there should not be two objects with the same identifier in the same configuration. There might be repeated identifiers in nested configurations, or in separate configurations, but not in the same configuration. This property is key for message delivery.

In general, a rewrite rule for an object system has the form

rl $⟨$Ob-1$⟩$ ... $⟨$Ob-k$⟩$ $⟨$Mes-1$⟩$ ... $⟨$Mes-n$⟩$ 
 => $⟨$Ob’-1$⟩$ ... $⟨$Ob’-j$⟩$ $⟨$Ob-k+1$⟩$ ... $⟨$Ob-m$⟩$ $⟨$Mes’-1$⟩$ ... $⟨$Mes’-p$⟩$ .
     

The operation getClass takes an object as argument and returns its actual class. See examples below. This operation will be particularly useful when combined with the inheritance relation (e.g., see the use of the getClass operation in the example in Section 7.6).

The remainder of the CONFIGURATION module provides definitions related to external objects (see Chapter 9).

6.1.1 Classes

Classes are defined with the keyword class, followed by the name of the class, followed by a bar ‘|’, followed 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 | a1 : $⟨$Sort-1$⟩$, ..., an : $⟨$Sort-n$⟩$ .
     

We can declare classes without attributes using syntax

class C .
     

As an example of class declaration, the class Account of bank account objects with a balance attribute, can be declared as follows:

class Account | bal : Int .
     

With this declaration, we are able to write account objects as < A : Account | bal : N >, with A a term of sort Oid and N a term of sort Int. An attribute name is any single token name that does not contain the underline character.

As another example, a class Person, with a name, an age, and a bank account as attributes can then be declared as follows:

class Person | name : String, age : Nat, account : Oid .
     

< A : Account | bal : 2000 > 
< P : Person | name : "Alice", age : 24, account : A >
     

As we saw in the previous section, all object-oriented modules have an operation getClass, defined in the CONFIGURATION module, that takes an object as argument and returns its actual class. Thus, for example,

getClass(< A-002 : Account | bal : 1000 >)
     

Class names have the same form as sort names (see Section 3.3). In particular, as we will explain in Section 7.4.3, class names may be parameterized in a way completely similar to parameterized sort names.

6.1.2 Messages

The syntax for message declarations is similar to the syntax for the declaration of operators, but using msg and msgs instead of op and ops, and having as result the sort Msg or a subsort of it. Thus, msg is used to declare a single message, and msgs may be used for declaring multiple messages. The user can introduce subsorts of the predefined sort Msg, so that it is possible to declare messages of different types. This may be useful for restricting the kind of messages that could be received by a particular type of object. As in the case of operators, messages can be overloaded and can be declared with operator attributes.

In the account example, the three kinds of messages involving accounts are credit, debit, and from_to_transfer_, whose user-definable syntax is introduced in the following declarations:

msgs credit debit : Oid Nat -> Msg . 
msg from_to_transfer_ : Oid Oid Nat -> Msg .
     

Notice the use of the Oid sort for specifying the addressee of a message, as in credit and debit, and for specifying the objects involved in a message, e.g., the source and the target accounts of an account transfer in the from_to_transfer_ message. As already pointed out, it is assumed that the message’s destination object is the first argument mentioned in the message declaration. This convention is needed by the object-message fair rewriting strategy (see Section 6.3). The behavior associated with the messages is then specified by rewrite rules in a declarative way (see Section 6.1.4). Given object identifiers Smith and A-002, the following term may represent a configuration with a person, his account, and a credit message sent to it.

< Smith : Person | name : "John", age : 34, account : A-002 > 
< A-002 : Account | bal : 1000 > 
credit(A-002, 100)
     

6.1.3 Class inheritance

Class inheritance is directly supported by Maude’s order-sorted type structure. Since class names are a particular case of sort names, 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, together with 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 SAVING-ACCOUNT of saving accounts introducing a subclass SavingAccount of Account with a new attribute rate recording the interest rate of the account.

class SavingAccount | rate : Float . 
subclass SavingAccount < Account .
     

In this example there is only one class immediately above SavingAccount, namely, Account. In general, however, a class $C$ may be defined as a subclass of several classes $D_1,\dots ,D_k$, i.e., multiple inheritance is supported. There is no restriction on the use of attributes with the same names. Of course, having classes with attributes with the same names may be a bad idea, but it is the responsability of the user to make it work. This may be aggravated with inheritance, since we may be adding attributes with the same name of an attribute in a superclass. If a class inherits from two different superclasses that share an attribute but with different associated sorts, then both attributes are inherited in the subclass. 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.

Objects in the class SavingAccount will have an attribute bal and can receive messages debiting, crediting and transferring funds exactly as any other object in the class Account. For example, the following object is a valid instance of class SavingAccount.

< A-002 : SavingAccount | bal : 5000, rate : 3.0 >
     

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

subclasses A B C < D E < F G H .
     

6.1.4 Object-oriented statements

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 6.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 [93] for a detailed explanation of the logical semantics of the object-oriented model of computation supported by Maude.

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 in the module ACCOUNT as follows:

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

The application of the debit rule on this configuration models the reception of the debit message by the Account object ’A-06238. Upon the reception of the message, the balance of the object changes as a result.

In the rules in the ACCOUNT module, all occurrences of objects include all their attributes. However, in object-oriented modules, it is possible not to mention in a given statement those attributes of an object that are not relevant for that statement. For example, 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.

To illustrate that not all attributes need to be cited in rules in object-oriented modules, let us consider the following simple example. A message for changing the age of a person defined by the class Person (introduced in Section 6.1.1) 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.

These rules, as any other statement defining the behavior of classes, will be inherited by their subclasses. In this case, inheritance means that these statements, will be applicable on instances of subclasses. Although the details will be introduced in the following sections, let us show an example.

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
   

Note that the SAVING-ACCOUNT module does not contain any rule. Specifically, we leave unspecified the rules for changing interest rates, or for computing and crediting the interest of an account according to its rate.¹ However, notice that the class SavingAccount inherits the attributes and the behavior of the Account class. For example, we now rewrite a configuration in the SAVING-ACCOUNT module, 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-28381 : SavingAccount | bal : 9200, rate : 3.0 > 
 < ’A-73728 : SavingAccount | bal : 6300, rate : 3.0 >
     

Note that Account and SavingAccount objects respond similarly to the rules specified.

As we will see in detail in Section 6.5, statements in object-oriented modules are transformed so that the intended behavior is obtained. For example, the exact same behavior specified for the Person class above could be expressed as follows:

vars A A’ : Nat . 
var  O : Oid . 
var  C : Person . 
var  Atts : AttributeSet . 
 
rl [change-age] : 
 < O : C | age : A’, Atts > 
 to O : new age A 
 => < O : C | age : A, Atts > .
     

Note that by using a variable C of type Person, which is a subsort of sort Cid, the rule may be applied to objects in subclasses of Person. Even though the value of the age attribute when the rule is applied is not relevant, to replace its value, it must appear in the lefthand side of the rule. Finally, notice the Atts attribute to take all other attributes that objects of the class have, which are left unchanged. This rule will be applied on objects of subclasses having additional attributes as well. Additional examples are presented, e.g., in Sections 6.2 and 7.6.

The transformation performed on the statements of object-oriented modules is explained in detail in Section 6.5. Although quite natural, it is important to keep in mind that the transformation is not carried out on all statements. Since, e.g., a rule may have in its right-hand side objects that are not in its left-hand side, replicated objects may show up in its right-hand side, the class of an object may change, and other situations in which no specific behavior is to be enforced, the user may choose to identify statements not to be transformed with the dnt (do not transform) attribute. Indeed, the attribute is required in some cases. Without it, Maude would produce advisories in these and other cases.

In summary, in order for a statement to be transformed, there are strict requirements governing the occurrence of objects. If a candidate statement does not meet these requirements, advisories will be produced and the statement will be placed in the resulting system module untransformed. Before enumerating these restrictions, let us consider an example. If we add a rule changing the class of an object, we will get advisories indicating the situation. If we load the module

omod WRONG-CHANGING-SAVING-ACCOUNT is 
 including SAVING-ACCOUNT . 
 var O : Oid . 
 rl < O : Account | > => < O : SavingAccount | > . 
endom
   

we get the following advisories:

Advisory: <standard input>, line 47 (omod WRONG-CHANGING-SAVING-ACCOUNT): 
   class argument SavingAccount in object instance < O : SavingAccount | none > 
   differing from class argument Account in lefthand side object instance 
   < O : Account | none > disables object completion. 
Advisory: <standard input>, line 47 (omod WRONG-CHANGING-SAVING-ACCOUNT): 
   transformation not performed for: 
 rl < O : Account | none > => < O : SavingAccount | none > .
     

With these advisories Maude is pointing out that there is something problematic in the rules, and that they will be left as provided by the user, without any transformation being applied on them. Note that we can understand the rule in different ways. Do we want it to be applicable only on objects of class Account or also to objects in subclasses? The subclass SavingAccount may have some additional attributes, what do we want to do with them? Without them objects will not be valid instances of that class, but Maude cannot add these attributes. Therefore, to eliminate these advisories, we can either change the rule as we wish or add a dnt attribute to force Maude to take it as such.

In other cases, many other questions may arise. In this case, possibly the sensible thing to do is to allow the change only to objects of the Account class, not to objects in subclasses, since they may already have a rate attribute, or have a different behavior that may conflict with this one.

 var O : Oid . 
 var Atts : AttributeSet . 
 
 rl < O : Account | Atts > 
 => < O : SavingAccount | rate : 3.0, Atts > 
 [dnt] .
     

A statement (mb/cmb/eq/ceq/rl/crl) that contains at least one occurrence of the object constructor operator (<_:_|_>) is a candidate for transformation unless it has the dnt attribute. The dnt attribute is ignored outside of object-oriented modules, and it disappears during translation to a system module—it is simply a flag that instructs the desugaring code to pass the statement into the system module without further consideration.

Before introducing the restrictions on the statements to be transformed, let us introduce some terminology:

• Within a candidate statement, two subterms with the object constructor on top, say < $t_1$ : $t_2$ | $t_3$ > and < $t_1^{\prime }$ : $t_2^{\prime }$ | $t_3^{\prime }$ >, are considered to be occurrences of the same object named $t_1^{″}$ if $t_1^{″}$ is the theory normal form of both $t_1$ and $t_1^{\prime }$.

• The term parts of a statement are of four kinds:

  pattern:

  the lefthand side of the statement,

  subject:

  the righthand side of an equation or rule,

  condition-pattern:

  the lefthand side of an assignment condition fragment or the righthand side of a rule condition fragment, and

  condition-subject:

  any other part of a condition fragment.

• If an object appears in the righthand side of a statement but not in its lefthand side, then $t$ is called a “new object.” If the object appears in both sides, possibly multiple times in the righthand side, then $t$ is called an “existing object.”

Then, the conditions any statement must satisfy in order to be transformed are:

• No objects must occur in a condition-pattern.

• An object cannot occur more than one time in the lefthand side of a statement.

• The class argument of each occurrence of an existing object must be identical and can only be either a class constant or a variable of a class sort.

• The attribute argument of an existing object can either be $a_1$ or an attribute set $a_1$, $...$, $a_n$ under the _,_AttributeSet operator. Here each $a_i$ must be one of (i) the constant none, (ii) a term headed by an attribute operator, or (iii) a variable X of sort AttributeSet. Only one such variable X is allowed in an attribute argument, and if such a variable appears in the attribute argument of some occurrence of an existing object $E$, it must appear in the attribute argument of every occurrence of that object $E$. Two terms $a_i$ and $a_j$ in the same attribute argument may not be headed by the same attribute operator.

Occurrences of existing objects are checked and may be transformed. New objects can occur in the subject or condition-subject parts and are neither analyzed nor transformed. The rationale is that such occurrences might have arbitrary code as second and third arguments to choose the class and attributes of a newly created object.

Let us conclude this section with the principles that have guided the design of the transformation:

• Transforming a statement in a way that surprises the user is worse than not providing a transformation.

• Transformations should be all or nothing at the statement level—transforming some occurrences of an object but not others will likely lead to confusion.

• Transformations should work for non-executable statements—it is reasonable to have a nonexec rule transformed and later use it at the metalevel or with the strategy language.

Please, find details on the transformation in Section 6.5.

6.1.5 Search on object-oriented modules

In the previous section, we have seen several examples on how to rewrite configurations of objects and messages. We can also search over configurations. For example, we can look for final states having objects of class Account with balance greater than or equal to $1000$ from a given initial configuration 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 >= 1000 . 
 
Solution 1 (state 7) 
states: 8  rewrites: 29 in 0ms cpu (0ms real) (72319 rewrites/second) 
C:Configuration --> < ’A-28381 : SavingAccount | bal : 9200, rate : 3.0 > 
                < ’A-73728 : SavingAccount | bal : 6300, rate : 3.0 > 
O:Oid --> ’A-06238 
N:Nat --> 1000 
 
No more solutions. 
states: 8  rewrites: 29 in 0ms cpu (0ms real) (53505 rewrites/second)
     

Note that the object in the search pattern explicitly specifies an object of class Account, and only one final state can be reached with an object of this class that satisfies the given condition. If we want to search for objects of class Account or any of its subclasses, we may write 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 : C:Account | bal : N:Nat, Atts:AttributeSet > 
         such that N:Nat >= 1000 . 
 
Solution 1 (state 7) 
states: 8  rewrites: 29 in 0ms cpu (0ms real) (113725 rewrites/second) 
C:Configuration --> < ’A-28381 : SavingAccount | bal : 9200, rate : 3.0 > 
                < ’A-73728 : SavingAccount | bal : 6300, rate : 3.0 > 
O:Oid --> ’A-06238 
C:Account --> Account 
Atts:AttributeSet --> (none).AttributeSet 
N:Nat --> 1000 
 
Solution 2 (state 7) 
states: 8  rewrites: 30 in 0ms cpu (0ms real) (88235 rewrites/second) 
C:Configuration --> < ’A-06238 : Account | bal : 1000 > 
                < ’A-73728 : SavingAccount | bal : 6300, rate : 3.0 > 
O:Oid --> ’A-28381 
C:Account --> SavingAccount 
Atts:AttributeSet --> rate : 3.0 
N:Nat --> 9200 
 
Solution 3 (state 7) 
states: 8  rewrites: 31 in 0ms cpu (0ms real) (76923 rewrites/second) 
C:Configuration --> < ’A-06238 : Account | bal : 1000 > 
                < ’A-28381 : SavingAccount | bal : 9200, rate : 3.0 > 
O:Oid --> ’A-73728 
C:Account --> SavingAccount 
Atts:AttributeSet --> rate : 3.0 
N:Nat --> 6300 
 
No more solutions. 
states: 8  rewrites: 31 in 0ms cpu (0ms real) (67099 rewrites/second)
     

In this case, we obtain three solutions, since any of the three objects in the configuration will satisfy the condition in the final state. Please, note that the object in the search pattern has a variable C:Account as class name, to match the Account class or any subclass of it, and a varible Atts:AttributeSet to gather the rest of the attributes of the object. Objects in the search pattern are left as given, and therefore, these variables are necessary if objects in any subclass are to be found. Note that in this way one can decide what exactly one wants to search for.

6.2 Example: a rent-a-car store

In order to further illustrate Maude’s object-oriented features, we specify a simple rent-a-car store example. Several rules in this specification have variables in their righthand sides or conditions not present in their lefthand sides; therefore, these rules are not directly executable by the rewrite engine and are declared as non-executable (with the nonexec attribute). In order to run the object-oriented system, we will have to use strategies; a possible such strategy will be presented in Section 10.1.1.

The regulations of the system, especially those that govern the rental processes, are the following:

1.

Cars are rented for a specific number of days, after which they should be returned.

2.

A car can be rented only if it is available.

3.

No credit is allowed; customers must pay cash.

4.

Customers must make a deposit at pick-up time of the estimated rental charges.

5.

Rental charges depend on the car class. There are three categories: economy, mid-size, and full-size cars.

6.

When a rented car is returned, the deposit is used to pay the rental charges.

7.

If a car is returned before the due date, the customer is charged only for the number of days the car has been used. The rest of the deposit is reimbursed to the customer.

8.

Customers who return a rented car after its due date are charged for all the days the car has been used, with an additional 20% charge for each day after the due date.

9.

Failure to return the car on time or to pay a debt may result in the suspension of renting privileges.

Let us begin with the static aspects of this system, i.e., with its structure. We can identify three main classes, namely the store, customer, and car classes. There are three kinds of cars: economy, mid-size, and full-size cars.

Customers may rent cars. This relationship may be represented by a Rental class which, in addition to references to the objects involved in the relationship, has some extra attributes. The system also requires some control over time, which we get with a class representing calendars that provides the current date and simulates the passage of time.

The Customer class has three attributes, namely, suspended, cash, and debt, to keep track of, respectively, whether she is suspended or not, the amount of cash that the customer currently has, and her debt with the store. Such a class is defined by the following Maude declaration:

class Customer | cash : Nat, debt : Nat, suspended : Bool .
     

The attribute available of the Car class indicates whether the car is currently available or not, and rate records the daily rental rate. We model the different types of cars for rent by three different subclasses, namely, EconomyCar, MidSizeCar and FullSizeCar.

class Car | available : Bool, rate : Nat . 
class EconomyCar . 
class MidSizeCar . 
class FullSizeCar . 
subclasses EconomyCar MidSizeCar FullSizeCar < Car .
     

Each object of class Rental will establish a relationship between a customer and a car, whose identifiers are kept in attributes customer and car, respectively. In addition to these, the class Rental is also declared with attributes deposit, pickUpDate, and dueDate to store, respectively, the amount of money left as a deposit by the customer, the date in which the car is picked up by the customer, and the date in which the car should be returned to the store.

class Rental | deposit  : Nat, dueDate : Nat, pickUpDate : Nat, 
            customer : Oid, car    : Oid .
     

Given the simple use that we are going to make of dates, we can represent them, for example, as natural numbers. Then, we may have a calendar object that keeps the current date and gets increased by a rewrite rule as follows:²

class Calendar | date : Nat . 
rl [new-day] : 
 < O : Calendar | date : F > 
 => < O : Calendar | date : F + 1 > .
     

Four actions can be identified in our example:

• a customer rents a car,

• a customer returns a rented car,

• a customer is suspended for being late in paying her debt or for being late in returning a rented car, and

• a customer pays (part of) her debt.

The rental of a car by a customer is specified by the car-rental rule below, which involves the customer renting the car, the car itself (which must be available, i.e., not currently rented), and a calendar object supplying the current date. The rental can take place if the customer is not suspended, that is, if her identifier is not in the set of identifiers of suspended customers of the store, and if the customer has enough cash to make the corresponding deposit. Notice that a customer could rent a car for less time she really is going to use it on purpose, because either she does not have enough money for the deposit, or prefers making a smaller deposit. According to the description of the system, the payment takes place when returning the car, although there is an extra charge for the days the car was not reserved.

crl [car-rental] : 
 < U : Customer | cash : M, suspended : false > 
 < I : Car | available : true, rate : Rt > 
 < C : Calendar | date : Today > 
 => < U : Customer | cash : M - Amnt > 
    < I : Car | available : false > 
    < C : Calendar | > 
    < A : Rental | pickUpDate : Today, dueDate : Today + NumDays, 
       car : I, deposit : Amnt, customer : U, rate : Rt > 
 if Amnt := Rt * NumDays /\ M >= Amnt 
 [nonexec] .
     

Note that, as already mentioned, those attributes of an object that are not relevant for a rule do not need to be mentioned. Attributes not appearing in the righthand side of a rule will maintain their previous values unmodified. Furthermore, since the variables A and NumDays appear in the righthand side or condition of the rule but not in its lefthand side, this rule has to be declared as nonexec. Note as well the use of the attributes customer and car in objects of class Rental, which makes explicit that a rental relationship is between the customer and the car specified by these attributes.

A customer returning a car late cannot be forced to pay the total amount of money due at return time. Perhaps she does not have such an amount of money in hand. The return of a rented car is specified by the rules below. The first rule handles the case in which the car is returned on time, that is, the current date is smaller than or equal to the due date, and therefore the deposit is greater than or equal to the amount due.

crl [on-date-car-return] : 
 < U : Customer | cash : M > 
 < I : Car | rate : Rt > 
 < A : Rental | customer : U, car : I, pickUpDate : PDt, 
              dueDate : DDt, deposit : Dpst > 
 < C : Calendar | date : Today > 
 => < U : Customer | cash : (M + Dpst) - Amnt > 
    < I : Car | available : true > 
    < C : Calendar | > 
 if (Today <= DDt) /\ Amnt := Rt * (Today - PDt) 
 [nonexec] .
     

The second rule deals with the case in which the car is returned late.

crl [late-car-return] : 
 < U : Customer | debt : M > 
 < I : Car | rate : Rt > 
 < A : Rental | customer : U, car : I, pickUpDate : PDt, 
              dueDate : DDt, deposit : Dpst > 
 < C : Calendar | date : Today > 
 => < U : Customer | debt : (M + Amnt) - Dpst > 
    < I : Car | available : true > 
    < C : Calendar | > 
 if DDt < Today   *** it is returned late 
    /\ Amnt := Rt * (DDt - PDt) 
             + ((Rt * (Today - DDt)) * (100 + 20)) quo 100 
 [nonexec] .
     

Debts may be paid at any time, the only condition being that the amount paid is between zero and the amount of money owed by the customer at that time.

crl [pay-debt] : 
 < U : Customer | debt : M, cash : N > 
 => < U : Customer | debt : M - Amnt, cash : N - Amnt > 
 if 0 < Amnt /\ Amnt <= N /\ Amnt <= M 
 [nonexec] .
     

Customers who are late in returning a rented car or in paying their debts “may” be suspended. The first rule deals with the case in which a customer has a pending debt, and the second one handles the case in which a customer is late in returning a rented car.

crl [suspend-late-payers] : 
 < U : Customer | debt : M, suspended : false > 
 => < U : Customer | suspended : true > 
 if M > 0 . 
 
crl [suspend-late-returns] : 
 < U : Customer | suspended : false > 
 < I : Car | > 
 < A : Rental | customer : U, car : I, dueDate : DDt > 
 < C : Calendar | date : Today > 
 => < U : Customer | suspended : true > 
    < I : Car | > 
    < A : Rental | > 
    < C : Calendar | > 
 if DDt < Today .