In a concurrent object-oriented system the concurrent state, which is usually called a configuration, has typically the structure of a multiset made up of objects and messages that evolves by concurrent ACU-rewriting28 using rules that describe the effects of communication events between some objects and messages. Intuitively, we can think of messages as "traveling" to come into contact with the objects to which they are sent, and then causing "communication events" by application of rewrite rules. Therefore, we can view concurrent object-oriented computation as deduction in rewriting logic; in this way, the configurations S that are reachable from a given initial configuration S0 are exactly those such that the sequent S0 --> S is provable in rewriting logic using the rewrite rules that specify the behavior of the given object-oriented system.
An object in a given state is represented as a term < O : C | a_1 : v_1 , ..., a_n : v_n > 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. An object with no attributes can be represented as < O : C | > Messages do not have a fixed syntactic form. Such syntactic form can be defined by the user for each application. The concurrent state of an object-oriented system is then a multiset of objects and messages, called a Configuration, with multiset union described with empty syntax __.
The following module CONFIGURATION defines the basic concepts of concurrent object systems. Note that the sorts Message and Attribute--as well as the sorts Oid and Cid of object and class identifiers--are for the moment left unspecified. They will become fully defined when the CONFIGURATION module is extended by specific object-oriented definitions in a given object-oriented module.
fmod CONFIGURATION is
sorts Oid Cid Attribute AttributeSet
Object Msg Configuration .
subsorts Object Msg < Configuration .
subsort Attribute < AttributeSet .
op none : -> AttributeSet .
op _,_ : AttributeSet AttributeSet -> AttributeSet
[assoc comm id: none] .
op <_:_| > : Oid Cid -> Object .
op <_:_|_> : Oid Cid AttributeSet -> Object .
op none : -> Configuration .
op __ : Configuration Configuration -> Configuration
[assoc comm id: none] .
endfm
In Full Maude, concurrent object-oriented systems can be defined by means of object-oriented modules--introduced by the keyword omod--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. In particular, all object-oriented modules implicitly include the above CONFIGURATION module and assume its syntax. For example, the ACCNT object-oriented module below specifies the concurrent behavior of objects in a very simple class Accnt of bank accounts, each having a bal(ance) attribute, which may receive messages for crediting or debiting the account, or for transferring funds between two accounts.
(omod ACCNT is
protecting QID .
protecting MACHINE-INT .
subsort Qid < Oid .
class Accnt | bal : MachineInt .
msgs credit debit : Oid MachineInt -> Msg .
msg transfer_from_to_ : MachineInt Oid Oid -> Msg .
vars A B : Oid .
vars M N N' : MachineInt .
rl [credit] : credit(A, M) < A : Accnt | bal : N >
=> < A : Accnt | bal : (N + M) > .
crl [debit] : debit(A, M) < A : Accnt | bal : N >
=> < A : Accnt | bal : (N - M) >
if N > M .
crl [transfer] : (transfer M from A to B)
< A : Accnt | bal : N > < B : Accnt | bal : N' >
=> < A : Accnt | bal : (N - M) >
< B : Accnt | bal : (N' + M) >
if N > M .
endom)