Objects and messages

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

  < O : C | $\langle$att-1$\rangle$, ... , $\langle$att-n$\rangle$ >

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=1\ldots n$. 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.