... sort^1.1

In Maude, types come in two flavors, called sorts and kinds (see Section 3, and the discussion of user-definable data in Section 1.1.2 below).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... sublanguage^1.2

This sublanguage is essentially an extension of the OBJ3 equational language [44], which has greatly influenced the design of Maude.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... rules.^1.3

As explained in Section 1.2, mathematically this is achieved by a logic inclusion, in which the functional world of equational theories is conservatively embedded in the nonfunctional, concurrent world of rewrite theories.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... any^1.4

Except for any combination including both associativity and idempotency, which is not currently supported.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... strategies^1.5

That is, internal to Maude's logic, in the sense of being definable by logical axioms.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... practice^1.6

In its fullest generality, it is well known that associative-commutative rewriting is an NP-complete problem. In programming practice, however, the patterns used as lefthand sides allow much more efficient matching, so that the theoretical limits only apply to ``pathological'' patterns not encountered in typical programming practice.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... system.^1.7

With additional operations, including a sequential composition operation for labeled transitions.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... them.^2.1

We do not display the `>' symbol that Maude adds at the beginning of each line.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...modules.^3.1

As explained in Section 6.3.1, specifications can also be given in theories, with a syntax entirely similar to that of modules, but theories, unlike modules, need not be executable.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... convenient.^3.2

In Full Maude, operator names in operator declarations must be given as single identifiers. Multiple-identifier names are also supported, but their equivalent single-identifier form must be used in their declarations.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... number,^3.3

The maximum allowed precedence value is $2^{31} - 1$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Boolean^4.1

By default, any Maude module imports the predefined BOOL module (see Section 7.1).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... follows:^4.2

Note that the source and target operations can equivalently be declared as

eq source(E ; S) = source(E) .

eq target(E ; S) = target(S) .

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... equations^4.3

Similar constructs are used in languages like ASF+SDF [25] and ELAN [6].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... results,^4.4

Note that, since when the predicate is not true it remains unevaluated, we have defined it at the kind level, that is, as a partial Boolean function; however, using the owise attribute (see Section 4.5.4) it is very easy to add an extra equation making _occurs-inner_ a total Boolean function.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...N:Nat.^4.5

Note that here we assume the declaration of the NatSeq concatenation operator __ as given in page , where it is declared to be associative. If we consider the declaration of this operator given in page , which is also declared to have nil as identity element, then we should write this equation as

op _occurs-inner_: [Nat] [NatSeq] -> [Bool] .

ceq N:Nat occurs-inner NS:NatSeq = true

if (I:Nat NS0:NatSeq N:Nat NS1:NatSeq M:Nat) := NS:NatSeq .

since the variables NS0:NatSeq and NS1:NatSeq might be instantiated to nil.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... idempotency.^4.6

Remember that the idem attribute cannot be specified together with an assoc attribute; therefore idempotency must in this case be specified explicitly by an equation.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...ansi-color.el.^4.7

There is a copy of this Emacs Lisp file with the Maude distribution just in case your Emacs distribution lacks it.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... command:^4.8

Try it in your terminal. The colors are not shown here for obvious reasons.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... modules.^4.9

More precisely, the scope of applicability of operator evaluation strategies is restricted to functional modules and to the equational part of system modules.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... so.^4.10

Indeed, several languages have conventions of this kind, including ASF+SDF [25].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... transformation^4.11

We thank Joseph Hendrix for pointing out this subtlety.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... equation^4.12

For the purposes of this discussion we can regard unconditional equations as the special case of conditional equations with empty condition, or with the condition $true = true$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... matches^4.13

Some authors would instead say that $u$ matches $t$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... position^4.14

We can represent a term $t$ as a tree, and use strings of numbers to identify positions $p$ in the tree, thus identifying subterms $t\vert _p$. For example, for $t = f(g(a), h(b))$, we have $t\vert _{\mathit{nil}} = t$, $t\vert _1 = g(a)$, $t\vert _{11} = a$, $t\vert _2 = h(b)$, and $t\vert _{21} = b$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... substitution^4.15

Note that if a variable $x$ has a sort $s$ instead of a kind, well sortedness of $\sigma$ means that $\sigma(x)$ must provably have sort $s$ (or lower) according to the equations $E$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... printed.^4.16

The cpu and real time information is not printed if the user has made use of the set show timing off command (see Section 16.7).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... shared^4.17

However, this sharing--i.e., treating the term as a dag instead of as a tree--is not done in a maximal way, so that all subterms that can be shared are; instead, term sharing is itself introduced incrementally by equational simplification, since Maude analyzes righthand sides of equations to identify its shared subterms. As explained by Eker in [37], in the presence of operator evaluation strategies (Section 4.4.7) term sharing has to be done carefully. Furthermore, when rewriting is performed with a rule in a system module (see Chapter 5), rather than with an equation, Maude will incrementally unshare those parts of the subject term needed to ensure that all possible rewrite with rules are considered. This is because rules in system modules need not be confluent. As a consequence, two identical subterms could be rewritten in totally different ways; but this of course would be prevented if they were to be shared.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... modules.^5.1

See [16, Chapter 16] for an interesting example of this kind: a concurrent implementation of a mobile language entirely programmed in Maude using sockets as external objects in the way explained in Section 8.4.1.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... conditional^5.2

For the purposes of this discussion, we view unconditional rules as a special case of conditional rules. The general admissibility requirement specializes then to a very easy requirement for an unconditional rule $t \rightarrow t'$, namely, that each variable of $t'$ must appear in $t$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... set^5.3

More precisely, each kind $k$ in $\Sigma$ corresponds to a different choice for a set of states, namely the set $T_{\Sigma/E\cup A,k}$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... out.^6.1

If a theory is imported using a mode other than including, the system gives an error message saying that the mode is being treated as if it were including. Other illegal importations give an error message saying that they are being ignored.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... declarations.^6.2

The only exception to this semantic equivalence between structured theories and their flattened form is the case in which a theory imports some modules, since any of the protecting or extending initiality requirements of the imported module and its submodules must be preserved. Those requirements would be lost if the whole structure were to be flattened.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... omitted.^6.3

In Full Maude (see Chapter 14), maps for all sorts in the source theory have to be explicitly given, even when they are identity maps.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... structured.^6.4

Notice that a structured sort name, such as List{Nat} for example, cannot be used as a view name, because it is not a single identifier; if desired, the user can write the single-identifier form List`{Nat`} as view name. The convention is totally general in Full Maude; see Section 14.3.2.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... $X_i \texttt{ :: } T_i$.^6.5

These renamed modules are visible as names when using the show modules command (see Section 16.8) and will be shared, but they cannot be referred to directly in module expressions.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... unnecessary.^6.6

In Section 14.3.2, we shall see how this naming convention can be easily extended to the case of Full Maude's parameterized views.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... integers.^6.7

In Section 14.3.2, we shall introduce the notion of parameterized views, a more convenient way of defining this kind of structures. Currently, parameterized views are only available in Full Maude.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... variable^6.8

Note that a variable in a monomial or polynomial is a constant, not a mathematical variable in the Maude sense. That is, in this example variables are understood as names. Of course, in Maude we can also define a variable X:X$Elt in the parameter sort to which variables belong as constants, or, more generally, variables such as P:Poly{R, X}. In this context such mathematical variables can be distinguished from variables as names by referring to them as metavariables.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... predicates.^7.1

The prec attribute in the last two operators assigns each of them an appropriate precedence value for parsing purposes (see Section 3.9).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... operators.^7.2

See Section 3.9 for information on precedence values and gathering patterns.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Generator.^7.3

For information on the the Mersenne Twister Random Number Generator, see http://www-personal.engin.umich.edu/~wagnerr/MersenneTwister.html.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... identifier^7.4

The syntax of Maude identifiers is discussed in Section 3.1.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... list.^7.5

We realize that terminology here can be a bit confusing, because in Maude sort is also a keyword for types.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... attempted.^8.1

Assuming, as it should be the case, that both object constructors have been declared with the object attribute.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... message.^8.2

There are program transformations that internalize conditions on message delivery to ensure a stronger fairness condition [56].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... number,^8.3

In this quite simple example, it is always "6".

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... mark^8.4

We use the character `#' as mark; therefore, the user data sent through the sockets should not contain such a character.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... terminating,^9.1

As usual, the ground Church-Rosser and termination assumptions should be understood modulo any axioms $A \subseteq E$ which in Maude are declared as equational attributes of operators.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... terminating,^9.2

Again, possibly modulo equational attributes $A \subseteq E\cup G$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...finite,^10.1

Note that this can happen even when $T_{\Sigma/E,k}$ is an infinite set: there is no requirement that $T_{\Sigma/E,k}$ is finite.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... section.^13.1

All these figures have been obtained running Maude during a hot summer night on a Linux platform with an Intel Pentium M760 2GHz processor and 1GB of memory.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... axiom.^13.2

Maude 1 did not allow multiple membership axioms on associative operators. In Maude 2 this works, although it will be extremely inefficient for large terms, since matching the extra membership essentially amounts to expanding out the equivalence class.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...PATH^14.1

Some fragments of this module have been discussed in Sections 3.5 and 4.3.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Maude.^14.2

The predefined module LOOP-MODE described in Section 12.1 is not supported in Full Maude.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... module:^14.3

Note the use of the equivalent single-identifier-form for on-the-fly declarations of variables; as we will see in Section 14.5, this is one of the syntactic restrictions of Full Maude.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... metarepresentation;^14.4

The Core Maude upModule function takes as second argument a Boolean value (see Section 11.4.1).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... same.^15.1

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, thus muddling them up.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... real-time^15.2

See [63,65] for a general methodology to specify real-time systems, including object-oriented ones, in rewriting logic.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... example:^15.3

The including CONFIGURATION+ . declaration in the shown module will be explained in Section 15.8.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... functions^15.4

An alternative possibility is to use the maps specified in the predefined MAP module in Section 7.13.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... follows:^15.5

We have simplified the transformation of object-oriented modules into system modules that originally appeared in [58].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.