Chapter 22
Object-Oriented Modules

In Full Maude, concurrent object-oriented systems can be defined by means of object-oriented modules—introduced by the keyword omod...endom—using a syntax more convenient than that of system modules, because it assumes acquaintance with the basic entities, such as objects, messages and configurations, and supports linguistic distinctions appropriate for the object-oriented case.

As in Core Maude, we may have specifications of object-oriented systems in system modules; for example, we could enter into Full Maude the system modules describing object-based systems discussed in Chapter 8 by enclosing them in parentheses. However, although Maude’s system modules are sufficient for specifying object-oriented systems, there are important conceptual advantages provided by Full Maude’s 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 at the Core Maude level were provided.

Object-oriented modules are however just syntactic sugar: they are internally transformed into system modules for execution purposes (Section 22.8). All object-oriented modules implicitly include the CONFIGURATION module (see Section 8.1), and thus assume the latter’s syntax. Recall that the module CONFIGURATION defines the basic concepts of concurrent object systems; among others, and besides the Configuration sort, it includes the declarations of sorts

22.1 Object-oriented systems

Some object-oriented concepts were introduced in Chapter 8. Here we recall some of them and then focus on the notions of class and inheritance, and on the additional syntactic facilities provided by Full Maude to support object-oriented programming.

22.1.1 Objects and messages

As in Core Maude, an object in a given state is represented as a term of the form

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

but Full Maude supports and enforces a specific choice for the syntax of attributes. Each attribute of sort Attribute consists of a name (attribute identifier), followed by a colon ‘:’ (with white space both before and after), followed by its value, which must have a given sort. Therefore, the Full Maude syntax for objects is

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

where O is the object’s name or identifier, C is its class identifier, the ai’s are the names of the object’s attribute identifiers, and the vi’s are the corresponding values, for i = 1n. In particular, an object with no attributes can be represented as

 
< O : C | >

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. Messages satisfying this requirement should be declared using the msg keyword. It is still possible to declare messages not following this requirement as operators of sort Msg; but, if declared as operators, no message attribute will be provided for them (see Sections 8.1 and 8.2). For example, the following declarations of messages are possible.

 
msg credit : Oid Nat -> Msg .
op left : -> Msg .

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.

22.1.2 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 .

In particular, we can declare classes without attributes using syntax

 
class C .

Class names have the same form as sort names. In particular, class names may be parameterized in a way completely similar to parameterized sort names (see Sections 6.3.3, 22.3, and 22.4).

As an example of class declaration, the class Account of bank account objects with a balance attribute, introduced in Section 8.1, is now declared as follows:

 
class Account | bal : Int .

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 .

In this case, a person has a reference to his/her account in an account attribute of sort Oid.

All Full Maude object-oriented modules have an operation class that takes an object as argument and returns its actual class. Thus, for example,

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

returns the class identifier Account. This operation will be particularly useful when combined with the inheritance relation (see the use of the getClass operation in the example in Section 22.5).

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 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. Note that, as explained in Chapter 8 for Core Maude, Full Maude also assumes 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 8.2). The behavior associated with the messages is then specified by rewrite rules in a declarative way (see Section 22.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)

22.1.3 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 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 associated with it in each of those superclasses must be the same.1 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 .

22.1.4 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 22.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 [103] 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 22.8 for more details). For instance, a message for changing the age of a person defined by the class Person (introduced in Section 22.1.2) may be defined as follows:

 
msg to_:‘newage_ : 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-time2 attribute 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.

22.2 Example: a rent-a-car store

In order to further illustrate Full 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 nonexecutable. In order to run the object-oriented system, we will have to use strategies; a possible such strategy will be presented in Section 22.6.

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 he is suspended or not, the amount of cash that the customer currently has, and his 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 > .

We do not worry here about the frequency with which the date gets increased, the possible synchronization problems in a distributed setting, or with any other issues related to the specification of time. See the papers [118120] on the specification of real-time systems in rewriting logic and Maude for a discussion on these issues.

Four actions can be identified in our example:

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 or equal to the due date, and therefore the deposit is greater 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] .

In this case, part of the deposit needs to be reimbursed. We can see that the Rental object disappears in the righthand side of the rule, that is, it is removed from the set of rentals and the availability of the car is restored.

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] .

In this case, the customer’s debt is increased by the portion of the amount due not covered by the deposit.

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 .

Since the system is not terminating, and there are several rules with variables in their righthand sides or conditions not present in their lefthand sides and not satisfying the admissibility conditions discussed in Section 5.3, strategies are necessary for controlling its execution. We can define many different strategies and use them in many different ways (see Section 17.7); a concrete possibility will be described later in Section 22.6.

22.3 Object-oriented parameterized programming

The notions of theory, view, and parameterized module (see Section 6.3) have been extended to the object-oriented case. In this section, we explain how to write object-oriented theories, views with object-oriented theories as sources and object-oriented modules or object-oriented theories as targets, and object-oriented parameterized modules with possibly object-oriented theories as parameters. In Section 22.4 we explain how the module operations available in Full Maude have been extended, so that they are also available on object-oriented modules. In particular, we will see how it is possible to rename an object-oriented module and to instantiate an object-oriented module parameterized by an object-oriented theory with a view having another object-oriented module as its target.

22.3.1 Theories

In addition to functional and system theories, Full Maude also supports object-oriented theories. Their structure is the same as that of object-oriented modules. Object-oriented theories can have classes, subclass relationships, and messages. These object-oriented notions may be useful for the definition of theories; for example, the following theory CELL specifies the theory of classes with at least one attribute of any sort.

 
(oth CELL is
sort Elt .
class Cell | contents : Elt .
endoth)

22.3.2 Views

For a view having an object-oriented theory as its source, the mapping of a class C in the source theory to a class C’ in the target is expressed with syntax

 
class C to C .

Attribute maps have the form

 
attr C . A to A .

where A is the name of an attribute of class C in the source theory and A’ is an attribute of the image class of C under the view.

The mapping of messages is expressed with syntax

 
msg M to M .

where M is a message identifier or a message identifier together with its arity and value sort. As for operators, a message map in which explicit arity and coarity are given affects the entire family of subsort-overloaded message declarations associated with the declaration of the given message.

22.3.3 Parameterized object-oriented modules

Like any other type of module, object-oriented modules can be parameterized, and, like sort names, class names may also be parameterized. The naming of parameterized classes follows the same conventions discussed in Section 6.3.3 for parameterized sorts.

As an example of an object-oriented parameterized module, we define a stack of elements. We define a class Stack{X} as a linked sequence of node objects. Objects of class Stack{X} have a single attribute first, containing the identifier of the first node in the stack. If the stack is empty, the value of the first attribute is null. Each object of class Node{X} has an attribute next holding the identifier of the next node—which should be null if there is no next node—and an attribute contents to store a value of sort X$Elt. Notice that node identifiers are of the form o(S,N), where S is the identifier of the stack object to which the node belongs, and N is a natural number. The messages push, pop and top have as their first argument the identifier of the object to which they are addressed, and will cause, respectively, the insertion at the top of the stack of a new element, the removal of the top element, and the sending of a response message elt containing the element at the top of the stack to the object making the request.

 
(omod OO-STACK{X :: TRIV} is
protecting INT .
protecting QID .
subsort Qid < Oid .
class Node{X} | next : Oid, contents : X$Elt .
class Stack{X} | first : Oid .
msg _push_ : Oid X$Elt -> Msg .
msg _pop : Oid -> Msg .
msg _top_ : Oid Oid -> Msg .
msg _elt_ : Oid X$Elt -> Msg .

op null : -> Oid .
op o : Oid Int -> Oid .

vars O O O’’ : Oid .
var E : X$Elt .
var N : Int .

rl [top] : *** top on a non-empty stack
< O : Stack{X} | first : O >
< O : Node{X} | contents : E >
(O top O’’)
=> < O : Stack{X} | >
< O : Node{X} | >
(O’’ elt E) .

rl [push1] : *** push on a non-empty stack
< O : Stack{X} | first : o(O, N) >
(O push E)
=> < O : Stack{X} | first : o(O, N + 1) >
< o(O, N + 1) : Node{X} |
contents : E, next : o(O, N) > .

rl [push2] : *** push on an empty stack
< O : Stack{X} | first : null >
(O push E)
=> < O : Stack{X} | first : o(O, 0) >
< o(O, 0) : Node{X} | contents : E, next : null > .

rl [pop] : *** pop on a non-empty stack
< O : Stack{X} | first : O >
< O : Node{X} | next : O’’ >
(O pop)
=> < O : Stack{X} | first : O’’ > .
endom)

Notice that top and pop messages are not received if the stack is empty.

We may want to define stacks storing not just data elements of a particular sort, but actually objects in a particular class. We can define an object-oriented module with the intended behavior as the parameterized module OO-STACK2 below, which is parameterized by the object-oriented theory CELL introduced in Section 22.3.1. Notice that the main difference with respect to the previous STACK version is in the attribute node, that keeps the identifier of the object where the contents can be found instead of the attribute contents that provided direct access to those contents.

 
(omod OO-STACK2{X :: CELL} is
protecting INT .
protecting QID .
subsort Qid < Oid .
class Node{X} | next : Oid, node : Oid .
class Stack{X} | first : Oid .
msg _push_ : Oid Oid -> Msg .
msg _pop : Oid -> Msg .
msg _top_ : Oid Oid -> Msg .
msg _elt_ : Oid X$Elt -> Msg .

op null : -> Oid .
op o : Oid Int -> Oid .

vars O O O’’ O’’’ : Oid .
var E : X$Elt .
var N : Int .

rl [top] : *** top on a non-empty stack
< O : Stack{X} | first : O >
< O : Node{X} | node : O’’ >
< O’’ : X$Cell | contents : E >
(O top O’’’)
=> < O : Stack{X} | >
< O : Node{X} | >
< O’’ : X$Cell | >
(O’’’ elt E) .

rl [push1] : *** push on a non-empty stack
< O : Stack{X} | first : o(O, N) >
(O push O’)
=> < O : Stack{X} | first : o(O, N + 1) >
< o(O, N + 1) : Node{X} |
next : o(O, N), node : O > .

rl [push2] : *** push on an empty stack
< O : Stack{X} | first : null >
(O push O’)
=> < O : Stack{X} | first : o(O, 0) >
< o(O, 0) : Node{X} | next : null, node : O > .

rl [pop] : *** pop on a non-empty stack
< O : Stack{X} | first : O >
< O : Node{X} | next : O’’ >
(O pop)
=> < O : Stack{X} | first : O’’ > .
endom)

22.4 Module operations on object-oriented modules

The module operations of summation, renaming, and instantiation have been extended so that they are also available on object-oriented modules.

22.4.1 Module summation and renaming

The summation and renaming of object-oriented modules is similar to their non-object-oriented counterparts. Renaming maps, however, are in this case available for mapping classes, attributes, and messages. Therefore, in addition to the renamings available in Core Maude, Full Maude also supports renaming maps of the form:

 
class identifier to identifier
attr class-identifier . attr-identifier to class-identifier
msg identifier to identifier
msg identifier : type-list -> type to identifier

We illustrate the renaming of object-oriented modules with the following example:3

 
Maude> (show module OO-STACK2 * (class Stack{X} to Stack{X},
class Node{X} to Node{X},
attr Stack{X} . first to head,
msg _elt_ to element,
sort Int to Integer) .)

omod OO-STACK2 * (sort Int to Integer,
msg _elt_ to element,
class Node‘{X‘} to Node‘{X‘},
class Stack‘{X‘} to Stack‘{X‘},
attr Stack‘{X‘} . first to head) {X :: CELL} is
protecting QID .
protecting INT * (sort Int to Integer) .
including CONFIGURATION+ .
including CONFIGURATION .
protecting BOOL .
subsort Qid < Oid .
class Node‘{X‘} | next : Oid, node : Oid .
class Stack‘{X‘} | head : Oid .
op null : -> Oid .
op o : Oid Integer -> Oid .
msg _pop : Oid -> Msg .
msg _push_ : Oid Oid -> Msg .
msg _top_ : Oid Oid -> Msg .
msg element : Oid X$Elt -> Msg .
rl < O:Oid : Stack{X}| head : O’:Oid >
< O’:Oid : Node{X}| next : O’’:Oid >
O:Oid pop
=> < O:Oid : Stack{X}| head : O’’:Oid >
[label pop] .
rl < O:Oid : Stack{X}| head : O’:Oid >
< O’:Oid : Node{X}| node : O’’:Oid >
< O’’:Oid : X$Cell | contents : E:X$Elt >
O:Oid top O’’’:Oid
=> < O:Oid : Stack{X}| none >
< O’:Oid : Node{X}| none >
< O’’:Oid : X$Cell | none >
element(O’’:Oid,E:X$Elt)
[label top] .
rl < O:Oid : Stack{X}| head : null >
O:Oid push O’:Oid
=> < O:Oid : Stack{X}| head : o(O:Oid,0)>
< o(O:Oid,0): Node{X}| next : null,node : O’:Oid >
[label push2] .
rl < O:Oid : Stack{X}| head : o(O:Oid,N:Integer)>
O:Oid push O’:Oid
=> < O:Oid : Stack{X}| head : o(O:Oid,N:Integer + 1)>
< o(O:Oid,N:Integer + 1): Node{X}|
next : o(O:Oid,N:Integer),node : O’:Oid >
[label push1] .
endom

22.4.2 Module instantiation

We show in this section how, by instantiating the object-oriented module OO-STACK2 given in Section 22.3.3, we can obtain a specification of a stack of banking accounts. We first specify a view Account from the object-oriented theory CELL (in Section 22.3.1) to the object-oriented module ACCOUNT (in Section 22.1.4).

 
(view Account from CELL to ACCOUNT is
sort Elt to Int .
class Cell to Account .
attr Cell . contents to bal .
endv)

Now we can do the following rewriting on the module resulting from the instantiation.

 
Maude> (rew in OO-STACK2{Account}
* (class Account to Account,
class Stack{Account} to Stack{Account},
class Node{Account} to Node{Account},
attr Stack{Account} . first to head,
attr Account . bal to balance,
msg _elt_ to element,
sort Int to Integer) :
< stack : Stack{Account} | head : null >
< A-73728 : Account | balance : 5000 >
< A-06238 : Account | balance : 2000 >
< A-28381 : Account | balance : 15000 >
(’stack push A-73728)
(’stack push A-06238)
(’stack push A-28381)
(’stack top A-06238)
(’stack pop) .)

result Configuration :
element(’A-28381,15000)
< A-06238 : Account | balance : 2000 >
< A-28381 : Account | balance : 15000 >
< A-73728 : Account | balance : 5000 >
< stack : Stack{Account}| head : o(’stack, 1)>
< o(’stack, 0) : Node{Account} | next : null, node : A-06238 >
< o(’stack, 1) : Node{Account} |
next : o(’stack, 0), node : A-73728 >

22.5 Example: extended rent-a-car store

This section describes a variant of the rent-a-car store example in Section 22.2 in which several interesting data structures are used to store relevant information.

Let us refine the specification of a rent-a-car store presented in Section 22.2 by adding the following regulations:

10.
When a rented car is returned, the deposit is used to pay the rental charges, which are calculated in accordance with the conditions at pick-up time.
11.
There are three different kinds of customers: staff, occasional, and preferred.
12.
Staff members and preferred customers benefit from special discounts in all rentals.
13.
A customer qualifies as “preferred” when the accumulated amount of money spent in the store by the customer is above a certain threshold.

The main differences introduced by these regulations are that we need to keep the conditions at pick-up time, so that the calculations at drop-off time are correct. We also need to distinguish the three different types of customers, with the possibility of an occasional customer being promoted to preferred if he spends a given amount of money.

As an alternative approach to the one followed previously in Section 22.2, we introduce a class Store of rental car stores, whose attributes represent the information concerning the general parameters of such stores: the rates applicable to each type of car, the discounts for each type of customer renting each type of car, the identifiers of the customers who are suspended, the amount of money above which occasional customers are qualified as preferred, the record with the amount of money spent in the store by each of the customers, and the daily penalty for late return (20%). In addition, attributes customers, cars, rentals, and calendar store the identifiers of the objects participating in the relationships with the Store composite object; those are directed binary relationships and therefore we need only store the identifiers of the subordinate objects as attributes of the object that references them.

 
class Store |
discounts : PFun{Tuple{Cid, Cid}, Nat},
payments : PFun{Oid, Nat},
penalty : Nat,
threshold : Nat,
suspended : Set{Oid},
rates : PFun{Cid, Nat},
customers : Set{Oid},
cars : Set{Oid},
rentals : Set{Oid},
calendar : Oid .

The information on rates, discounts, and money spent is modeled by attributes of sort PFun of partial functions4 (see Section 6.3.7), associating the appropriate values to each of the different agents involved. The rates for the different cars are stored in the attribute rates, of sort PFun{Cid, Nat}, that associates the per-day rate to be charged to a customer for renting a given type of car. Thus, assuming that Rts is a variable of sort PFun{Cid, Nat}, with value the partial function assigning the appropriate rates to each type of car, we have that Rts[FullSizeCar] is the per-day rate for renting a full size car. If we want to increase this rate by, say 20%, we can use the expression

 
Rts[FullSizeCar -> Rts[FullSizeCar] * (100 + penalty) / 100]

with penalty a constant equal to 20. The discounts applied to each customer on each type of car and the amount of the purchases of each customer are stored, respectively, in attributes payments and discounts. The set of the identifiers of the customers who are suspended is stored in an attribute suspended of sort Set{Oid}. The predefined sorts Oid and Cid are used for object identifiers and class identifiers, respectively.

This specification will allow us, for instance, to easily “compose” systems with different particular details (e.g., discounts may change from one store to another), allowing them to easily co-exist.

The rest of the classes can be specified as follows:

 
class Customer | cash : Nat, debt : Nat .
class Staff .
class OccasionalCust .
class PreferredCust .
subclasses OccasionalCust PreferredCust Staff < Customer .

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

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

The different actions may then be defined as follows:

 
crl [car-rental] :
< U : Customer | cash : M >
< I : Car | available : true > *** the car is available
< V : Store | suspended : US,
rates : Rts, discounts : Dscnts, calendar : C,
cars : (I, IS), customers : (U, SS), rentals : RS >
< C : Calendar | date : Today >
=> < U : Customer | cash : sd(M, Amnt) >
< I : Car | available : false >
< V : Store | rentals : (A, RS) >
< C : Calendar | >
< A : Rental | pickUpDate : Today, dueDate : Today + NumDays,
car : I, deposit : Amnt, customer : U,
rate : Rt, discount : Dscnt >
if not U in US *** the customer is not suspended
/\ Rt := Rts[getClass(< I : Car | >)]
/\ Dscnt := Dscnts[(getClass(< U : Customer | >),
getClass(< I : Car | >))]
/\ Amnt := sd(Rt, Dscnt) * NumDays
/\ M >= Amnt *** enough cash to make a deposit
[nonexec] .

Notice the use of customer and car attributes in objects of class Rental, which makes explicit that a rental relationship is between the customer and the car specified by these attributes. Likewise for attributes customers, cars, and calendar of object V of class Store, which indicate that the customer, car and calendar appearing on the rule should be known to the store. After the car-rental action, the rental is added to the set of rentals kept by the store.

Rules may be applied to objects of the classes specified in the rules or of any of their subclasses. Remember that the function getClass takes an object as argument and returns its actual class (see Section 22.1.2); for example, the getClass function applied to an object of the form < ’c123 : MidSizeCar | ... > returns MidSizeCar, and not Car. Finally, notice the use of matching equations of the form t := t’ in the condition (see Section 4.3).

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. Notice that the rate and discount to be used in the calculation of the amount due are those at pick-up time, which are stored as attributes of the Rental object.

 
crl [on-date-car-return] :
< U : Customer | cash : M >
< I : Car | >
< A : Rental | customer : U, car : I, rate : Rt, discount : Dscnt,
pickUpDate : Ppdt, dueDate : Ddt, deposit : Dpst >
< V : Store | payments : Pmnts, cars : (I, IS),
customers : (U, SS), calendar : C, rentals : (A, RS) >
< C : Calendar | date : Today >
=> < U : Customer | cash : M + sd(Dpst, Amnt) >
< I : Car | available : true >
< V : Store | rentals : RS,
payments : (if Pmnts[U] == undefined *** no record for customer
then Pmnts[U -> Amnt]
else Pmnts[U -> ((Pmnts[U]) + Amnt)]
fi) >
< C : Calendar | >
if (Today <= Ddt) /\ Amnt := sd(Rt, Dscnt) * sd(Today, Ppdt) .

In this case, the deposit is greater than the amount due and therefore part of the deposit needs to be reimbursed. Note also that the Store object keeps a record of the amount of money spent by each customer in the store, and thus it must be updated accordingly. We can see how the Rental object disappears in the righthand side of the rules: it is removed from the set of rentals known to the store and the availability of the car is restored.

The second rule deals with the case in which the car is returned late. The amount to be paid is calculated at drop-off time, but the rate and discount to be used, those at pick-up time, may have changed when returning the car.

 
crl [late-car-return] :
< U : Customer | debt : M >
< I : Car | >
< A : Rental | customer : U, car : I, rate : Rt, discount : Dscnt,
pickUpDate : Ppdt, dueDate : Ddt, deposit : Dpst >
< V : Store | payments : Pmnts, penalty : Pnlt, rentals : (A, RS),
cars : (I, IS), customers : (U, SS), calendar : C >
< C : Calendar | date : Today >
=> < U : Customer | debt : M + sd(Amnt, Dpst) >
< I : Car | available : true >
< V : Store | rentals : RS,
payments : (if Pmnts[U] == undefined
then Pmnts[U -> Dpst]
else Pmnts[U -> ((Pmnts[U]) + Dpst)]
fi) >
< C : Calendar | >
if Ddt < Today *** it is returned late
/\ Amnt := (sd(Rt, Dscnt) * sd(Ddt, Ppdt))
+ (((sd(Rt, Dscnt) * sd(Today, Ddt))
* (100 + Pnlt)) quo 100) .

In this case the customer’s debt is increased by the portion of the amount due not covered by the deposit.

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

 
crl [pay-debt] :
< V : Store |
payments : Pmnts, customers : (U, SS), calendar : C >
< U : Customer | debt : M, cash : N >
< C : Calendar | date : Today >
=> < V : Store | payments : Pmnts[U -> ((Pmnts[U]) + Amnt)] >
< U : Customer | debt : sd(M, Amnt), cash : sd(N, Amnt) >
< C : Calendar | >
if 0 < Amnt /\ Amnt <= N /\ Amnt <= M
[nonexec] .

We are assuming that, if there is a debt, then there has been a previous payment, and therefore there is already a record for that customer.

The text says that customers who are late in returning a rented car or in paying their debts “may” be suspended. However, nothing is said about the reasons for taking such a decision or when they should be suspended, that is, a customer could be suspended right after the car is returned without having paid all the charges, after some grace days, or never. In practice there will be fixed criteria, as, for example, suspending customers that are two days late, or two months.

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] :
< V : Store | suspended : US, customers : (U, SS) >
< U : Customer | debt : M >
=> < V : Store | suspended : (U, US) >
< U : Customer | >
if (not U in US) and M > 0 .

 
crl [suspend-late-returns] :
< V : Store | suspended : US, cars : (I, IS),
customers : (U, SS), calendar : C >
< U : Customer | >
< I : Car | >
< A : Rental | customer : U, car : I, dueDate : F >
< C : Calendar | date : Today >
=> < V : Store | suspended : (U, US) >
< U : Customer | >
< I : Car | >
< A : Rental | >
< C : Calendar | >
if (not U in US) and F < Today .

The upgrade in the status of a customer can then be modeled with the following rule:

 
crl [upgrade-to-preferred] :
< U : OccasionalCust | cash : M, debt : N >
< V : Store | threshold : Thrshld, payments : Pmnts,
customers : (U, SS), calendar : C >
< C : Calendar | date : Today >
=> < U : PreferredCust | cash : M, debt : N >
< V : Store | >
< C : Calendar | >
if (Pmnts[U]) >= Thrshld .

In this rule, a customer object U of subclass OccasionalCust becomes of subclass PreferredCust when the accumulated amount of purchases exceeds the store’s threshold. The partial function stored in the attribute payments gives us the amount of money spent by each customer. In Maude, objects changing their classes must show all their attributes in the righthand sides of the rules.

As in the simpler rent-a-car system, the presence of nonterminating rules and of rules with new variables in the righthand side requires some kind of strategy for the execution of the system; we give an example of such a strategy in the next section.

22.6 A strategy for sequential rule execution

Strategies are necessary for controlling the execution of rules that are not terminating, or that do not satisfy the admissibility conditions discussed in Section 5.3. A simple but interesting strategy may be one that allows us to execute a given sequence of rules, that is, to accomplish sequentially a series of actions from a particular initial state. We introduce in this section such a generic strategy and illustrate its use by applying it for executing the systems specified in Sections 22.2 and 22.5. Dealing with strategies may become cumbersome, since we need to handle terms and modules at different levels of reflection, and expressions may become quite hard to read and handle. We show in this section how the upModule and upTerm functions and the down command introduced in Section 21.4 can help in alleviating this difficulty.

A strategy is represented as a sequence of rule applications. We instantiate the predefined module LIST with pairs formed by a rule label representing the rule to be applied, and a substitution to partially instantiate the variables in such a rule before its application. The pairs are obtained using the generic tuple construction described in Section 21.3.1. Thus, to get the module expression LIST{Tuple{Qid, Substitution}}, given the predefined view Qid and the parameterized view Tuple, that we have already used in the partial functions example of Section 6.3.7, we only need to define a view Substitution from TRIV to META-LEVEL.

 
(view Substitution from TRIV to META-LEVEL is
sort Elt to Substitution .
endv)

This construction is put to work in the module REW-SEQ below. The operator rewSeq in this module takes the metarepresentation of a module, the metarepresentation of a term, and a list of pairs (each formed by a rule label and a substitution); the term obtained in this way is rewritten by applying the given rules sequentially, using in their applications their corresponding partial substitutions.

 
(mod REW-SEQ is
including META-LEVEL .
protecting LIST{Tuple{Qid, Substitution}} .

var M : Module .
var T : Term .
var L : Qid .
var S : Substitution .
var LLS : List{Tuple{Qid, Substitution}} .

op rewSeq :
Module Term List{Tuple{Qid, Substitution}} -> [Term] .

rl [seq] : rewSeq(M, T, (L, S) LLS)
=> rewSeq(M,
getTerm(metaXapply(M, T, L, S, 0, unbounded, 0)), LLS) .

rl [seq] : rewSeq(M, T, nil) => T .
endm)

The rules to be applied here are part of the module given as first argument. The strategy starts with the term given as initial state, which is replaced in each recursive call by the term representing the state obtained after the application of the next rule in the sequence (see Section 17.6.4). When all the rules have been applied, thus reaching the empty list as third argument, the current state is returned as the resulting final state.

We illustrate the use of the rewSeq strategy by applying a sequence of rules on a configuration of the rent-a-car system specified in Section 22.2. Let RENT-A-CAR-STORE be the name of the module containing the specification of such a system, and let StoreConf be a configuration of objects defined in the following module.

 
(fmod RENT-A-CAR-STORE-TEST is
pr RENT-A-CAR-STORE .

op StoreConf : -> Configuration [memo] .
eq StoreConf
= < C1 : Customer | cash : 5000, debt : 0, suspended : false >
< C2 : Customer | cash : 5000, debt : 0, suspended : false >
< A1 : EconomyCar | available : true, rate : 100 >
< A3 : MidSizeCar | available : true, rate : 150 >
< A5 : FullSizeCar | available : true, rate : 200 >
< C : Calendar | date : 0 > .
endfm)

The StoreConf configuration consists of two clients C1 and C2, three cars A1, A3 and A5, and a calendar object C. Now, let StoreStrat be a sequence of pairs (rule label - substitution) that defines the strategy declared in the following module as a sequence of actions:

 
(fmod REW-SEQ-TEST is
pr REW-SEQ .

op StoreStrat : -> List{Tuple{Qid, Substitution}} [memo] .
eq StoreStrat
= (’car-rental,
U:Oid <- ’’C1.Qid ; *** size car A3 for 2 days
I:Oid <- ’’A3.Qid ;
NumDays:Int <- s_^2[’0.Zero] ;
A:Oid <- ’’a0.Qid)
(’new-day, none) *** two days pass
(’new-day, none)
(’on-date-car-return, none) *** car A3 is returned
(’new-day, none)
(’car-rental, *** client C1 rents the full
U:Oid <- ’’C1.Qid ; *** size car A5 for 1 day
I:Oid <- ’’A5.Qid ;
NumDays:Int <- s_^1[’0.Zero] ;
A:Oid <- ’’a1.Qid)
(’new-day, none) *** two days pass
(’new-day, none)
(’late-car-return, none) *** car A5 is returned
(’new-day, none)
(’suspend-late-payers, none) *** client C1 is suspended
(’new-day, none)
(’new-day, none)
(’pay-debt, *** client C1 pays 100$
Amnt:Int <- s_^100[’0.Zero]) .
endfm)

Comments on the righthand side of the code above explain the sequence of rules defining the strategy. Basically, the execution trace specified consists of client C1 renting two cars, one of which is returned on time and the other one is returned late. After the second car is returned, the client is suspended for being late in his payments. The client then pays part of his debt. Note how the passage of time is modeled by the application of the rule new-day.

Now, in order to execute the system specifications using this strategy, we just need to use rewSeq to apply the given rules sequentially, using their corresponding partial substitutions in their applications. Note how the first two arguments are metarepresented with the upModule and upTerm functions, since they need to be the metarepresentations of the actual module and term, respectively.

 
Maude> (down RENT-A-CAR-STORE :
rew rewSeq(upModule(RENT-A-CAR-STORE-TEST),
upTerm(RENT-A-CAR-STORE-TEST, StoreConf),
StoreStrat) .)

result Configuration :
< C : Calendar | date : 8 >
< C1 : Customer | suspended : true, debt : 140, cash : 4400 >
< C2 : Customer | suspended : false, debt : 0, cash : 5000 >
< A1 : EconomyCar | rate : 100, available : true >
< A3 : MidSizeCar | rate : 150, available : true >
< A5 : FullSizeCar | rate : 200, available : true >

We can see in this configuration that eight days have passed, after which the client C1 is suspended. The client C1 has paid a total of $600 (= 2 × 150 + 200 + 100), and has still a debt of $140 (= 200 + 20 % 200 100).

The same strategy can be used to execute the extended specification in Section 22.5, contained in a module named EXTENDED-RENT-A-CAR-STORE. First, we define a module with an initial configuration ExtStoreConf.

 
(fmod EXTENDED-RENT-A-CAR-STORE-TEST is
pr EXTENDED-RENT-A-CAR-STORE .

op ExtStoreConf : -> Configuration [memo] .
eq ExtStoreConf
= < S : Store |
discounts :
(((Staff, EconomyCar), 20),
((Staff, MidSizeCar), 30),
((Staff, FullSizeCar), 40),
((OccasionalCust, EconomyCar), 0),
((OccasionalCust, MidSizeCar), 0),
((OccasionalCust, FullSizeCar), 0),
((PreferredCust, EconomyCar), 10),
((PreferredCust, MidSizeCar), 15),
((PreferredCust, FullSizeCar), 20)),
payments : empty, penalty : 0,
threshold : 1000, suspended : empty,
rates : ((EconomyCar, 100),
(MidSizeCar, 150),
(FullSizeCar, 200)),
customers : (’C1, C2),
cars : (’A1, A3, A5),
rentals : empty, calendar : C >
< C1 : Staff | cash : 5000, debt : 0 >
< C2 : OccasionalCust | cash : 5000, debt : 0 >
< A1 : EconomyCar | available : true >
< A3 : MidSizeCar | available : true >
< A5 : FullSizeCar | available : true >
< C : Calendar | date : 0 > .
endfm)

Now we execute a command completely analogous to the previous one, obtaining a resulting state that shows how, after eight days, client C1 has paid $500, and has a debt of $60.

 
Maude> (down EXTENDED-RENT-A-CAR-STORE :
rew rewSeq(upModule(EXTENDED-RENT-A-CAR-STORE),
upTerm(EXTENDED-RENT-A-CAR-STORE, ExtStoreConf),
StoreStrat) .)
result Configuration :
< A1 : EconomyCar | available : true >
< A3 : MidSizeCar | available : true >
< A5 : FullSizeCar | available : true >
< C : Calendar | date : 8 >
< C1 : Staff | cash : 4500, debt : 60 >
< C2 : OccasionalCust | cash : 5000, debt : 0 >
< S : Store | calendar : C,
cars : (’A1, A3, A5),
customers : (’C1, C2),
discounts : (((OccasionalCust, EconomyCar), 0),
((OccasionalCust, FullSizeCar), 0),
((OccasionalCust, MidSizeCar), 0),
((PreferredCust, EconomyCar), 10),
((PreferredCust, FullSizeCar), 20),
((PreferredCust, MidSizeCar), 15),
((Staff, EconomyCar), 20),
((Staff, FullSizeCar), 40),
((Staff, MidSizeCar), 30)),
payments : (’C1, 500),
penalty : 0,
rates : ((EconomyCar, 100),
(FullSizeCar, 200),
(MidSizeCar, 150)),
rentals : empty,
suspended : C1,
threshold : 1000 >

22.7 Model checking a round-robin scheduling algorithm

In this section we present a specification of a round-robin scheduling algorithm, and the mutual exclusion and guaranteed reentrance properties are proven about it. Both the algorithm and the property guaranteing that all processes reenter their critical sections are parameterized by the number of processes. We use Maude’s model checker to prove the mutual exclusion and guaranteed reentrance properties. As we said in Section 21.2 , to use the MODEL-CHECKER module, or any other Core Maude module, we just need to make sure that it has been loaded; we suggest loading the model-checker.maude file before starting Full Maude.

We first give a specification of natural numbers modulo. Since we want to be able to have any number of processes, we define the NAT/ module parameterized by the functional theory NZNAT#, which requires a constant of sort Nat. Thus, having a view, say 5 from TRIV to NZNAT# mapping # to the natural number 5, the module expression NAT/{5} specifies the natural numbers modulo 5.

 
(fth NZNAT# is
protecting NAT .
op # : -> NzNat .
endfth)

 
(fmod NAT/{N :: NZNAT#} is
sort Nat/{N} .
op ‘[_‘] : Nat -> Nat/{N} [ctor] .
op _+_ : Nat/{N} Nat/{N} -> Nat/{N} .
op _*_ : Nat/{N} Nat/{N} -> Nat/{N} .
vars N M : Nat .
ceq [N] = [N rem #] if N >= # .
eq [N] + [M] = [N + M] .
eq [N] * [M] = [N * M] .
endfm)

The round-robin scheduling algorithm is specified in the module RROBIN below. Processes are represented as objects of class Proc, which may be in wait or critical mode, meaning that a process may be either in its critical section or waiting to enter into it. The process getting the token, which is represented as the message go, can enter its critical section. Once a process gets out of its critical section it forwards the token to the next process. The init operator sets up the initial configuration for a given number of processes. Note that Nat/{N} is made a subsort of Oid, making in this way natural numbers modulo N valid object identifiers.

 
(omod RROBIN{N :: NZNAT#} is
protecting NAT/{N} .

sort Mode .
ops wait critical : -> Mode [ctor] .

subsort Nat/{N} < Oid .

class Proc | mode : Mode .
msg go : Nat/{N} -> Msg .

var N : Nat .

rl [enter] :
go([N])
< [N] : Proc | mode : wait >
=> < [N] : Proc | mode : critical > .

rl [exit] :
< [N] : Proc | mode : critical >
=> < [N] : Proc | mode : wait >
go([s(N)]) .

op init : -> Configuration .
op make-init : Nat/{N} -> Configuration .

ceq init = go([0]) make-init([N]) if s(N) := # .
ceq make-init([s(N)])
= < [s(N)] : Proc | mode : wait > make-init([N])
if N < # .
eq make-init([0]) = < [0] : Proc | mode : wait > .
endom)

For proving mutual exclusion and guaranteed reentrance, we declare the propositions inCrit and twoInCrit in the module CHECK-RROBIN below (see Chapter 12 for a discussion on the use of Maude’s model checker). The property inCrit takes a Nat/{N} as argument, thus making this property parameterized by the number of processes, and is true when such a process is in its critical section. The property twoInCrit is true if any two processes are in their critical sections simultaneously. Mutual exclusion will be proved directly below, while for proving guaranteed reentrance we use the auxiliary formula guaranteedReentrance, which allows us to specify the property of all processes reentering their critical sections in exactly 2N steps, for N the number of processes. For a formula F, nextIter F returns O…O F (where O denotes the modal next operator), which specifies that the property is true in the next iteration, that is, 2N steps later. Note that the expression 2 * # will become two times N once the module is instantiated.

 
(omod CHECK-RROBIN{N :: NZNAT#} is
pr RROBIN{N} .
inc MODEL-CHECKER .
inc SATISFACTION .
ex LTL-SIMPLIFIER .
inc LTL .

subsort Configuration < State .

op inCrit : Nat/{N} -> Prop .
op twoInCrit : -> Prop .

var N : Nat .
vars X Y : Nat/{N} .
var C : Configuration .
var F : Formula .

eq < X : Proc | mode : critical > C |= inCrit(X) = true .
eq < Y : Proc | mode : critical > < Y : Proc | mode : critical > C
|= twoInCrit = true .

op guaranteedReentrance : -> Formula .
op allProcessesReenter : Nat -> Formula .
op nextIter_ : Formula -> Formula .
op nextIterAux : Nat Formula -> Formula .

eq guaranteedReentrance = allProcessesReenter(#) .

eq allProcessesReenter(s N)
= (inCrit([s N]) -> nextIter inCrit([s N])) /\
allProcessesReenter(N) .
eq allProcessesReenter(0) = inCrit([0]) -> nextIter inCrit([0]) .

eq nextIter F = nextIterAux(2 * #, F) .

eq nextIterAux(s N, F) = O nextIterAux(N, F) .
eq nextIterAux(0, F) = F .
endom)

Note that the LTL formula describing the guaranteedReentrance property is not a single LTL formula, but an infinite parametric family of formulas

guaranteedReentrance = {allProcessesReenter(n) | n ∈ ℕ}.

The use of equations in the above CHECK-RROBIN parameterized module allows us to define this infinite family of formulas by means of a few recursive equations. When this module is instantiated for a concrete value of n, we then obtain the concrete LTL formula allProcessesReenter(n) for that n.

We now prove mutual exclusion and guaranteed reentrance for the case of five processes using the model checker.

 
(view 5 from NZNAT# to NAT is
op # to term 5 .
endv)

 
Maude> (reduce in CHECK-RROBIN{5} :
modelCheck(init, [] ~ twoInCrit) .)
result Bool :
true

 
Maude> (reduce in CHECK-RROBIN{5} :
modelCheck(init, [] guaranteedReentrance) .)
result Bool :
true

Of course the answer depends on the property checked and is not always true. The following example shows how the model checker gives a counterexample as result when trying to prove that, for a configuration of five processes, process [1] is in its critical section three steps after it was in it.

 
Maude> (red in CHECK-RROBIN{5} :
modelCheck(init, [] (inCrit([1]) -> O O O inCrit([1]))) .)
result ModelCheckResult :
counterexample(
{go([0]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : critical > <[1]: Proc | mode : wait >
<[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit}
{go([1]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : critical >
<[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit}
{go([2]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
<[2]: Proc | mode : critical > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit},
{go([3]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
<[2]: Proc | mode : wait > <[3]: Proc | mode : critical >
<[4]: Proc | mode : wait >, exit}
{go([4]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
<[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
<[4]: Proc | mode : critical >, exit}
{go([0]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : critical > <[1]: Proc | mode : wait >
<[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit}
{go([1]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : critical >
<[2]: Proc | mode : wait > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit}
{go([2]) <[0]: Proc | mode : wait >
<[1]: Proc | mode : wait > <[2]: Proc | mode : wait >
<[3]: Proc | mode : wait > <[4]: Proc | mode : wait >, enter}
{<[0]: Proc | mode : wait > <[1]: Proc | mode : wait >
<[2]: Proc | mode : critical > <[3]: Proc | mode : wait >
<[4]: Proc | mode : wait >, exit})

22.8 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:5

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 22.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 [44] 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.