Maude: specification and programming in rewriting logic

Maude: speci$cation and programming in rewriting logic M. Clavela , F. Dur)anb , S. Ekerc , P. Lincolnc , N. Mart)0-Olietd; ∗, J. Meseguerc , J.F. Quesadae/ aDepartamento de Filosofa, Universidad de Navarra, Spain bETSI Informatica, Universidad de Malaga, Spain cComputer Science Lab , SRI International, 333 Ravenswood Ave., Menlo Park, CA, 94025 USA dFacultad de Matematicas, Universidad Complutense, Madrid, Spain eCentro d e I nformatica Cient-ca d e Andaluca, S evilla, S pain Abstract Maude i s a h igh-level l anguage a nd a h igh-performance s ystem s upporting e xecutable speci$-cation a nd d eclarative p rogramming i n r ewriting l ogic. S ince r ewriting l ogic contains e quational l ogic, Maude a lso s upports e quational s peci$cation a nd p rogramming i n its s ublanguage o f f unc-tional modules a nd t heories. The u nderlying e quational l ogic chosen f or Maude i s membership e quational l ogic, t hat h as s orts, s ubsorts, o perator overloading, a nd p artiality d e$nable b y mem-bership a nd e quality c onditions. Rewriting l ogic is r e:ective, i n t he s ense o f b eing a ble t o e xpress i ts o wn metalevel a t t he o bject l evel. Re:ection i s s ystematically e xploited i n Maude e ndowing t he l anguage with p owerful metaprogramming c apabilities, i ncluding b oth u ser-de$nable module o perations a nd declarative s trategies t o g uide t he d eduction p rocess. This p aper e xplains a nd i llustrates with e xamples t he main c oncepts o f Maude’s l anguage d esign, i ncluding i ts u nder-lying logic, f unctional, s ystem a nd o bject-oriented modules, a s well a s p arameterized modules, theories, a nd v iews. We a lso e xplain h ow Maude s upports r e:ection, metaprogramming a nd in-ternal s trategies. The p aper o utlines t he p rinciples u nderlying t he Maude s ystem implementation, i ncluding i ts s emicompilation t echniques. We c onclude with s ome r emarks about a pplications, work o n a f ormal e nvironment f or Maude, a nd a mobile l anguage extension o f Maude. Keywords: Maude; Rewriting l ogic; F unctional modules; S ystem modules; P arameterization; Re:ection; Internal s trategies 1. Introduction Maude [14,15] is a high-level language and high-performance system supporting both equational and rewriting logic computation for a wide range of applications. Maude has been in:uenced in important ways by OBJ3 [37]; in particular, Maude’s equational logic sublanguage essentially contains OBJ3 as a sublanguage. The main differences from OBJ3 at the equational level are a much greater performance, and a richer equational logic, namely, membership equational logic [48], that extends OBJ3’s order-sorted equational logic [36]. The key novelty of Maude is that — besides eFciently supporting equational computation and algebraic speci$cation in the OBJ style — it also supports rewriting logic computation. Rewriting logic [43] is a logic of concurrent change that can naturally deal with state and with highly nondeterministic concurrent computations. It has good properties as a :exible and general semantic framework for giving semantics to a wide range of languages and models of concurrency [47,35,11,53]. In particular, it supports very well concurrent object-oriented computation. This is re:ected in Maude’s design by providing special syntax for object-oriented modules. Since the computational and logical interpretations of rewriting logic are like two sides of the same coin, the same reasons making it a good semantic framework at the computational level make it also a good logical framework at the logical level, that is, a metalogic in which many other logics can be naturally represented and implemented [41]. Consequently, some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for diMerent logics, theorem provers, languages, and models of computation. Maude’s functional modules are theories in membership equational logic [9,48], a Horn logic whose atomic sentences are equalities t=tand membership assertions of the form t:s, stating that a term thas sort s. Such a logic extends order-sorted equational logic [36], and supports sorts, subsort relations, subsort polymorphic overloading of operators, and de$nition of partial functions with equationally de$ned domains. Maude’s functional modules are assumed to be Church–Rosser and terminating; they are executed by the Maude engine according to the rewriting techniques and operational semantics developed in [9]. Membership equational logic is a sublogic of rewriting logic [43]. A rewrite theory is a pair (T; R) with Ta membership equational theory, and Ra collection of labelled and possibly conditional rewrite rules involving terms in the signature of T. Maude’s system modules are rewrite theories in exactly this sense. The rewrite rules r:t→t in Rare not equations. Computationally, they are interpreted as local transition rules in a possibly concurrent system. Logically, they are interpreted as inference rules in a logical system. Rewriting in (T; R) happens modulo the equational axioms in T. Maude supports rewriting modulo all combinations of associativity, commutativity, and identity. The rules in Rneed not be Church–Rosser and need not be terminating. Many diMerent rewriting paths are then possible; therefore, the choice of appropriate strategies is crucial for executing rewrite theories. In Maude, such strategies are not an extralogical part of the language. They are instead internal strategies de$ned by rewrite theories at the metalevel. This is because rewriting logic is re<ective [12,20] in the precise sense of having a -nitely presented universal theory Uthat can simulate any $nitely presented rewrite theory. Since Uis representable in itself, we can then achieve a “re:ective tower” with an arbitrary number of levels of re:ection. Maude eFciently supports this re:ective tower through its META-LEVEL module, which makes possible not only the declarative de$nition and execution of user-de$nable rewriting strategies, but also many other metaprogramming applications. In particular, it is possible to de$ne and execute within the logic an extensible module algebra supporting the OBJ style of parameterized programming [37], with highly generic and reusable modules. The basic idea is that META-LEVEL is extended with new data types for: parameterized modules; theories, with loose semantics, to state formal requirements in parameters; views, to bind parameter theories to their instances; and module expressions, instantiating, transforming, and composing parameterized modules. All such new types and operations are de$ned in Maude itself. This, together with the explicit access to modules as terms provided by re:ection, makes the corresponding module algebra completely open, and easily extensible by new module operations and transformations [28]. Maude also supports object-oriented modules, with convenient syntax for object-oriented applications. All applications typical of equational programming and algebraic speci$cation are conveniently and eFciently supported through Maude’s sublanguage of functional modules. In fact, the paper [48] argues that Maude’s equational logic, namely, membership equational logic, is so expressive — yet eFciently implementable — as to oMer very good advantages as a logical framework for a very wide range of algebraic speci$cation languages based on both total and partial equational logic formalisms. However, many Maude applications go beyond equational logic. System modules support general rewriting logic applications. The important area of concurrent and distributed objectbased system speci$cation and prototyping is supported by object-oriented modules. In addition, re:ection makes possible many novel metaprogramming and metalanguage applications, and is extremely valuable in the use of rewriting logic as a logical and semantic framework [41]. The rewriting logic research program has shown good signs of vitality, including three international workshops [46,39,34], over 200 research papers (see the references in [47,49,51,50]), and three language implementation eMorts, namely ELAN [40,8,7] in France, CafeOBJ [23,24,25] in Japan, and Maude. Therefore, Maude should be seen as our contribution to the broader collective eMort of building good language implementations for rewriting logic. In this regard, a key distinguishing feature of Maude is its systematic and eFcient use of re<ection, exploiting the fact that rewriting logic is re:ective, a feature that makes Maude remarkably extensible and powerful, and that allows many advanced metaprogramming and metalanguage applications. This paper constitutes a revised and extended presentation of concepts and ideas previously introduced in several conference papers [19,13,30,16,31]. Those papers have provided snapshots of the language versions at diMerent moments, while this journal version focuses on the main concepts in a (mostly) version-independent way. However, we do not develop here complete presentations of the underlying logics, providing instead bibliographic references where the reader can $nd more details. The reader is assumed to have some knowledge of algebraic speci$cation concepts (as surveyed for example in the recent book [1]). For a more introductory presentation of Maude, the reader is advised to read the Maude tutorial [15], where the main features of the language are introduced in an incremental way by means of a sequence of detailed examples. More language details can also be found in the Maude manual [14], which has large amounts of version-dependent information. We plan to keep the manual as an evolving online document re:ecting new versions of the language as they are developed. The Maude system, the just mentioned tutorial and manual, a collection of examples and case studies, and a list of related papers are available (free of charge) at http:==maude.csl.sri.com. 2. Membership equational logic and functional modules Maude is a declarative language based on rewriting logic, but rewriting logic has its underlying equational logic as a parameter. There are, for example, unsorted, manysorted, and order-sorted versions of rewriting logic, each containing the previous version as a special case. In particular, the underlying equational logic chosen for Maude is membership equational logic, a conservative extension of both order-sorted equational logic and partial equational logic with existence equations [48,9]. It supports partiality, subsort relations, operator overloading, and error speci$cation. 2.1. Membership equational logic Asignature in membership equational logic is a triple =(K; ; S) with Ka set of kinds,(K; ) a many-sorted (although it is better to say “many-kinded”) signature, and S={Sk}k∈KaK-kinded set of sorts.An-algebra is then a (K; )-algebra Atogether with the assignment to each sort s∈Skof a subset As⊆Ak. Intuitively, the elements in sorts are the good, or correct, or non-error, or de$ned, elements, whereas the elements without a sort are error or unde$ned elements. In general, a total function at the kind level restricts only to a partial function at the level of sorts. Atomic formulas are either -equations,ormemberships of the form t:s, where the term thas kind kand s∈Sk. General sentences are Horn clauses on these atomic formulas, quanti$ed by $nite sets of K-kinded variables. That is, they are either conditional equations (∀X)t=tif  i ui=vi∧ j wj:sj or conditional memberships of the form (∀X)t:sif  i ui=vi∧ j wj:sj: Such memberships are a generalization of sort constraints [52] and can be used to specify partial functions, that become de$ned when their arguments satisfy certain equational and membership conditions. Order-sorted notation can also be used for convenience, and we do so in Maude. Thus, a subsort declaration s¡ sabbreviates the conditional membership axiom (∀x)x:sif x:s. Similarly, an operator declaration f:s1:::s n→s0at the sort level corresponds to an operator declaration at the kind level together with the conditional membership axiom (∀x1;:::;x n)f(x1;:::;x n): s0if x1:s1∧ ··· ∧ xn:sn. Membership equational logic has all the usual good properties: soundness and completeness of appropriate rules of deduction, initial and free algebras, relatively free algebras along theory morphisms, and so on [48]. 2.2. Functional modules In Maude, functional modules are equational theories in membership equational logic satisfying some additional requirements. Computation in a functional module is accomplished by using the equations as rewrite rules until a canonical form is found. This is the reason why the equations must satisfy the additional requirements of being Church–Rosser, terminating, and sort decreasing [9]. This guarantees that all terms in an equivalence class modulo the equations will rewrite to a unique canonical form, and that this canonical form can be assigned a sort that is smaller than all other sorts assignable to terms in the class. Since Maude supports rewriting modulo equational theories such as associativity, commutativity, and identity, all that we say has to be understood for equational rewriting modulo such axioms [22]. We explain now the syntactic treatment in Maude of kinds, variables, and conditions in conditional equations and membership axioms. With respect to kinds, Maude does automatic kind inference from the sorts declared by the user and their subsort relations, but kinds are not explicitly named; instead, a kind kis identi$ed with the set Skof its sorts, interpreted as an equivalence class modulo the equivalence relation generated by the subsort ordering, that is, two sorts are in this equivalence relation if and only if they belong to the same connected component in the poset of sorts. Therefore, for any s∈Sk;[s] denotes the kind k=Sk, understood as the connected component of the poset of sorts to which s belongs. As an example that will be developed step by step in this section, let us consider as given a graph speci$cation sorts Node Edge . ops source target : Edge -> Node . with operations giving the source and target nodes of each edge, as well as speci$c edge and node constants that need not concern us here. Then, we extend such a speci$cation by declaring a sort Path of paths over the graph, together with a partial concatenation operator, and appropriate source and target functions over paths as follows, where the subsort declaration states that edges are “unitary” paths. sort Path . subsort Edge < Path . op _;_ : [Path] [Path] -> [Path] . ops source target : Path -> Node . This illustrates the idea that in Maude sorts are user-de$ned, while kinds are implicitly associated with connected components of sorts and are considered as “error supersorts”. The Maude system also lifts automatically to kinds all the operators involving sorts of the corresponding connected components to form error expressions. Such error expressions allow us to give expressions to be evaluated the bene$t of the doubt: if, when they are simpli$ed, they have a legal sort, then they are ok; otherwise, the fully simpli$ed error expression is returned as an error message. Variables in a Maude module do not have to be declared in variable declarations; they can appear directly in terms. A variable consists of an identi$er composed of a name, followed by a colon, followed by either a sort or a kind name. For example, P:Path is a variable of sort Path. Variable declarations are still allowed for convenience; for example, the declaration var P :Path allows using the name Pas an abbreviation for the variable P:Path. Equational conditions in conditional equations and memberships are made up of individual equations t=tand memberships t:sby a binary conjunction connective /\ which is assumed associative. Furthermore, the concrete syntax of equations in conditions has two variants, namely, ordinary equations t=t’, and matching equations t:=t’. For example, the following axioms express the condition de$ning path concatenation and the associativity of this operator: var E : Edge . varsPQRS:Path . cmbE;P:Path if target(E) = source(P) . ceq(P;Q);R=P;(Q;R) if target(P) = source(Q) /\ target(Q) = source(R) . The conditional membership axiom (introduced by the keyword cmb) states that an edge concatenated with a path is also a path when the target node of the edge coincides with the source node of the path. This has the eMect of de$ning path concatenation as a partial function on paths, although it is total on the kind [Path] of “confused paths”. Instead of giving the above associativity equation explicitly (by means of the conditional equation introduced by the keyword ceq), if we wanted to apply the axioms modulo associativity, we could have declared an associativity equational attribute in the declaration of the operator: op _;_ : [Path] [Path] -> [Path] [assoc] . Assuming variables P,E, and Sdeclared as above, source and target functions over paths are de$ned by means of matching equations in conditions as follows: ceq source(P) = source(E) ifE;S:=P. ceq target(P) = target(S) ifE;S:=P. Matching equations are mathematically interpreted as ordinary equations; however, operationally they are treated in a special way and they must satisfy special requirements. Note that the variables Eand Sin the above matching equation do not appear in the left-hand sides of the corresponding conditional equations. In the execution of these equations, these new variables become instantiated by matching the term E;S against the subject term bound to the variable P. In order for this match to decide the equality with the ground term bound to P, the term E;Smust be a pattern. Given a functional module M, we call a term tan M-pattern if for any well-formed substitution such that for each variable xin its domain the term (x) is in canonical form with respect to the equations in M, then (t) is also in canonical form. A suFcient condition for tto be an M-pattern is the absence of uni$ers between its nonvariable subterms and left-hand sides of equations in M. Ordinary equations t=tin conditions have instead the usual operational interpretation, that is, for the given substitution ,(t) and (t) are both reduced to canonical form and compared for equality, modulo the equational axioms speci$ed in the module’s operator declarations such as associativity, commutativity, and identity. All conditional equations t=tif C1∧ ··· ∧Cnin a functional module Mhave to satisfy the following admissibility requirements,1ensuring that all the extra variables will become instantiated by matching: (1) vars(t)⊆vars(t)∪ n  j=1 vars(Cj): (2) If Ciis an equation ui=u ior a membership ui:s, then vars(Ci)⊆vars(t)∪ i−1  j=1 vars(Cj): (3) If Ciis a matching equation ui:= u i, then uiis an M-pattern and vars(u i)⊆vars(t)∪ i−1  j=1 vars(Cj): The satisfaction of the conditions is attempted sequentially from left to right. Since matching takes place modulo equational attributes, in general many diMerent matches may have to be tried until a match of all the variables satisfying the condition is found. As mentioned before, we expect functional modules to be Church–Rosser and terminating membership equational logic speci$cations in the sense of [9, Section 10:1]. The 1These requirements include as a special case what are called properly oriented and right stable 3-CTRSs in [61], when each equation si=tiin their conditions is expressed as a matching equation ti:= si. above admissibility requirements and the Church–Rosser and termination assumptions are dropped for functional theories (see Section 4.2) which support the full generality of the logic. In membership equational logic the Church–Rosser property of terminating and sortdecreasing equations is indeed equivalent to the con:uence of their critical pairs in an appropriately generalized sense [9]. Furthermore, both equality and membership of a term in a sort are then decidable properties [9]. That is, the equality and membership predicates are computable functions. We can then use the metatheorem of Bergstra and Tucker [3] to conclude that such predicates are themselves speci$able by Church– Rosser and terminating equations as Boolean-valued functions. This has the pleasant consequence of allowing us to include inequalities t=tand negations of membership assertions not(t:s) in conditions of equations and of membership axioms, since such seemingly negative predicates can also be axiomatized inside the logic in a positive way, provided that we have a subspeci$cation of (not necessarily free) constructors in which to do it, and that the speci$cation is indeed Church–Rosser, terminating, and sort decreasing. Of course, in practice they do not have to be explicitly axiomatized, since they are built into the implementation of rewriting deduction in a much more eFcient way. Indeed, by default, Maude modules implicitly import a prede$ned BOOL module providing Boolean values true and false, and operators _and_,_or_, and not_. In addition, this imported prede$ned module provides the semantic equality operator _==_ checked by equational simpli$cation, its negation _=/=_, a conditional operator if_then_else_fi, and a membership predicate _::_. For example, the associativity property could also be speci$ed as ceq(P;Q);R=P;(Q;R) if target(P) == source(Q) and target(Q) == source(R) . More generally, a Boolean expression bis allowed to appear as a conjunct in an equational condition as a shorthand for the equation b = true. If a collection of (conditional) equations is Church–Rosser and terminating, given an expression, no matter how the equations are used from left to right as simpli$cation rules, any reduction strategy will reach a normal form and moreover we will always reach the same $nal result. However, even though the $nal result may be the same, some orders of evaluation can be considerably more eFcient than others. It may therefore be useful to have some way of controlling the way in which equations are applied by means of strategies. Typically, a functional language is either eager, or lazy with some strictness analysis added for eFciency, and the user has to live with whatever the language provides. Maude adopts OBJ3’s :exible method of user-speci$ed evaluation strategies on an operator-by-operator basis [37], adding some improvements to the OBJ3 approach to ensure a correct implementation [33]. For an n-ary operator fsuch strategies are speci$ed as lists i1:::i mof numbers, with im= 0, and 06ij6n, for j=1;:::;m−1. For example, the default bottom-up eager strategy given in Maude to an n-ary operator f, when no strategy is explicitly declared by the user, is (1 ::: n 0), stating that in evaluating a term f(t1;:::;t n), the subterms t1;:::;t nare evaluated in this order before applying the equations for fto the whole term. Similarly, the strategy given to if_then_else_fi is(10230),stating that it is enough to evaluate the Boolean condition in the $rst argument before trying the evaluation of the whole term. In addition to improving eFciency, operator strategies allow us to compute with in$nite data structures which are evaluated on demand; for example, a lazy “cons” list constructor may have strategy (0). The paper [33] documents in detail the operational semantics and the implementation techniques for Maude’s operator evaluation strategies; their concrete syntax as attributes in operator declarations is explained in [14]. As in the OBJ family of languages [37], functional modules can be unparameterized, or they can be parameterized with functional theories as their parameters (see Section 4for more details). Functional theories are also membership equational logic theories, but they do not need to be Church–Rosser and terminating. They have a loose interpretation, in the sense that any algebra satisfying the equations and membership axioms in the theory is an acceptable model. On the other hand, the semantics of an unparameterized functional module is the initial algebra speci$ed by its theory. The semantics of a parameterized functional module is the free functor associated to the inclusion of the parameter theory into the body of the parameterized module [48,27]. For example, the semantics of a list module LIST(X :: TRIV) parameterized over the simple parameter theory TRIV with only one sort Elt (see Section 4.3)isthe functor sending each set to the algebra of lists over this set. Similarly, the semantics of a sorting module SORTING(Y :: POSET) parameterized over the POSET functional theory (see Section 4.2) is the functor sending each poset to the algebra of lists for that poset with a sorting function. 2.3. Example: arrays as lists of pairs We $nish this section with a functional module illustrating Maude’s support for mix$x user-de$nable syntax and for module hierarchies (see Section 4.1). An array of integers is represented as a list of pairs of integers, where the $rst component of each pair corresponds to the array position and the second to the value in that position. A list of pairs of this kind is the representation of an array if either it is empty, or the $rst components of the pairs are all diMerent and the positions of consecutive pairs are consecutive numbers. The $rst module imports the prede$ned module MACHINE-INT, providing integers and usual arithmetic operations on them. Then, it de$nes a sort IntPair for pairs of integers with (_,_) as only constructor 2(notice the ctor attribute specifying that this operator is a constructor of the sort). These pairs are used as components of lists, de$ned with the concatenation operator __ as the main constructor, declared with both an attribute assoc for associativity, and an attribute id: nil for the empty list nil 2Since parentheses are normally used for disambiguation, in order to correctly declare this operation, it is necessary to write (( , )). Under these circumstances, the default strategy in the Maude interpreter applies the rules in a top-down rule fair way, 4always reducing to canonical form using E before applying any rule in R. More speci$cally, before the application of each rewrite rule, the expression is simpli$ed to its canonical form by applying the equations E modulo A; then, the rule is applied to such a simpli$ed expression modulo the axioms Aaccording to the default strategy. 3.3. Example: blocks world As another example of a system module, we specify a simple concurrent system, the blocks world, a typical example in arti$cial intelligence circles. In this version there is a table on top of which we have the blocks, which can be moved by means of three actions. A block is represented as a record with three $elds: a label identifying the block (given by a quoted identi$er, as provided in the prede$ned module QID), the label of the block on top (or the constant clear if there is none), and the label of the block below (or the constant table if there is none because the block is on the table). A state of the blocks world is then represented as a set of such blocks that is consistent in the sense that each block has a diMerent label, and that for each pair of blocks aand b,ifais on top of b, then bis below a. In the module below we only make explicit the $rst part of the consistency check (all block labels are diMerent). mod BLOCKS-WORLD is protecting QID . sorts Up Down . subsorts Qid < Up Down . op clear : -> Up [ctor] . op table : -> Down [ctor] . sort Block . op {label:_, under:_, on:_} : Qid Up Down -> Block [ctor] . sort State . subsort Block < State . op empty : -> State [ctor] . op __ : State State -> [State] [ctor assoc comm id: empty] . op free : Qid State -> Bool . varsXYZ:Qid. vars S S’ : State . var U U’ : Up . vars O O’ : Down . cmb {label: X, under: U, on: O} S : State if free(X, S) . eq free(X, empty) = true . 4“Top-down” means that each rewrite is attempted beginning at the top of the term, so that any position rewritten does not have a position above it that could also have been rewritten. A limited form of fairness is achieved by keeping the rules in a circular list, and moving a rule to the end of the list after it has been applied. Fig. 1. Initial and $nal states in a world with three blocks. ceq free(X, S) = X =/= Y and free(X, S’) if {label: Y, under: U, on: O} S’ := S . rl [move] : {label: X, under: clear, on: Z} {label: Z, under: X, on: O} {label: Y, under: clear, on: O’} => {label: X, under: clear, on: Y} {label: Z, under: clear, on: O} {label: Y, under: X, on: O’} . rl [unstack] : {label: X, under: clear, on: Z} {label: Z, under: X, on: O} => {label: X, under: clear, on: table} {label: Z, under: clear, on: O} . rl [stack] : {label: X, under: clear, on: table} {label: Z, under: clear, on: O} => {label: X, under: clear, on: Z} {label: Z, under: X, on: O} . endm The rule move moves a block Xsitting on top of another block Zto the top of block Y. The rule unstack moves a block Xsitting on top of another block Zto the table, whereas the rule stack does the reverse action. Consider for example the states described in Fig. 1. The initial state Ion the left and the $nal state Fon the right are, respectively, described by the following two terms of sort State: {label: ’a, under: ’c, on: table} {label: ’c, under: clear, on: ’a} {label: ’b, under: clear, on: table} {label: ’c, under: ’b, on: table} {label: ’b, under: ’a, on: ’c} {label: ’a, under: clear, on: ’b} The fact that the “sequential plan” (in a self-explanatory intuitive notation) unstack(c; a); stack(b; c); stack(a; b) moves the blocks from state Ito state Fcorresponds directly to a sequence of computational rewrite steps applying the corresponding rewrite rules. 3.4. Object-oriented modules Among the many concurrent systems that we can specify as system modules in Maude, concurrent object-oriented systems are an important subclass [44]. In a concurrent object-oriented system the concurrent state, which is usually called a con-guration, has typically the structure of a multiset made up of objects and messages that evolves by concurrent rewriting modulo associativity, commutativity and identity, using rules that describe the eMects of communication events between objects and messages. An object in a given state is represented in Maude as a term <O:C|a1:v1,:::,an:vn> where Ois the object’s name or identi$er, Cis its class identi$er, the ai’s are the names of the object’s attribute identi-ers, and the vi’s are the corresponding values. Messages do not have a $xed syntactic form; such syntactic form is de$ned 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 de$nes the basic concepts of concurrent object systems. Note that the sorts Msg and Attribute, as well as the sorts Oid and Cid of object and class identi$ers, are left unspeci$ed. They will become fully de$ned when the CONFIGURATION module is extended by speci$c object-oriented de$nitions 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 [ctor] . op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none] . op <_:_|_> : Oid Cid AttributeSet -> Object [ctor] . op none : -> Configuration [ctor] . op __ : Configuration Configuration -> Configuration [ctor assoc comm id: none] . endfm Concurrent object-oriented systems are de$ned in Maude 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 con$gurations, 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. Classes are de$ned with the keyword class, followed by the name of the class C, and by a list of attribute declarations separated by commas. Each attribute declaration has the form a:S, where ais an attribute identi$er and Sis the sort in which the values of the attribute range; that is, class declarations have the form class C|a1:S1,:::,an:Sn. The rewrite rules in an object-oriented module specify in a declarative way the behavior associated with the messages. The multiset structure of the con$guration provides the top-level distributed structure of the system and allows concurrent application of the rules [44]. By convention, the only object attributes made explicit in a rule are those relevant for that rule. In particular, the attributes mentioned only on the left-hand side of the rule are preserved unchanged, the original values of attributes mentioned only on the right-hand side of the rule do not matter, and all attributes not explicitly mentioned are left unchanged. The following object-oriented module gives an object-oriented speci$cation of the blocks world described in Section 3.3. A block is now represented as an object with two attributes, under, saying whether it is under another block or it is clear, and on, saying whether the block is on top of another block or is on the table. omod OO-BLOCKS-WORLD is protecting QID . sorts BlockId Up Down . subsorts Qid < BlockId < Oid . subsorts BlockId < Up Down . op clear : -> Up [ctor] . op table : -> Down [ctor] . class Block | under : Up, on : Down . varsXYZ:BlockId . rl [move] : < X : Block | under : clear, on:Z> < Z : Block | under:X> < Y : Block | under : clear > =><X:Block | on:Y> < Z : Block | under : clear > < Y : Block | under:X>. rl [unstack]:<X:Block | under : clear, on:Z> < Z : Block | under:X> =><X:Block | on : table > < Z : Block | under : clear > . rl [stack] : < X : Block | under : clear, on : table > < Z : Block | under : clear > =><X:Block | on:Z> < Z : Block | under:X>. endom The states Iand Fin Fig. 1are, respectively, described now by the following two con$gurations: < ’a : Block | under : ’c, on : table > < ’c : Block | under : clear, on : ’a > < ’b : Block | under : clear, on : table > < ’c : Block | under : ’b, on : table > < ’b : Block | under : ’a, on : ’c > < ’a : Block | under : clear, on : ’b > Class inheritance is directly supported by Maude’s order-sorted type structure. A subclass declaration C<C’in an object-oriented module is just a particular case of a subsort declaration. The eMect of a subclass declaration is that the attributes, messages, and rules of all the superclasses as well as the newly de$ned attributes, messages, and rules of the subclass characterize the structure and behavior of the objects in the subclass. Suppose that the blocks world is further re$ned so that now blocks can have colors, but we still want the rules for manipulating blocks to remain the same. This is trivially achieved by class inheritance as illustrated by the following module. omod OO-BLOCKS-WORLD+COLOR is including OO-BLOCKS-WORLD . sort Color . ops red blue yellow : -> Color [ctor] . class ColoredBlock | color : Color . subclass ColoredBlock < Block . endom In this example, there is only one class immediately above ColoredBlock, namely, Block, but a class may in general be de$ned as a subclass of several classes, i.e., multiple inheritance is also 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, when an attribute occurs in two diMerent superclasses, then the sort associated to it in each of those superclasses must be the same. Then, 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. The semantics of object-oriented modules is entirely reducible to that of system modules, in the sense that each object-oriented module can be translated into a corresponding system module whose semantics is by de$nition that of the original object-oriented module [44,27]. In particular, rewrite rules are modi$ed to make them applicable to all objects of the given classes and of their subclasses, that is, not only to objects whose class identi$ers are those explicitly given. However, although Maude’s object-oriented modules are in this way reduced to system modules, there are of course important conceptual advantages provided by the syntax of object-oriented modules. This syntax allows the user to think and express his or her thoughts in object-oriented terms whenever such a viewpoint seems best suited for the problem at hand. Those conceptual advantages would be lost if only system modules were provided. For example, in an object-oriented con$guration we have objects that maintain their identity across their state changes, and the notions of fairness adequate for them are more specialized than those appropriate for arbitrary system modules. This is because, since each object has an individual identity, fairness should now be localized to individual objects and messages, which should not be starved even when other similar objects and messages are rewritten. In summary, the approach taken in Maude is to provide a logical semantics for concurrent object-oriented programming by taking rewriting logic as its foundation, and then de$ning in a rigorous way higher-level object-oriented concepts above such a foundation. The papers [44,45] provide good background on such foundations. Talcott’s papers [62–65] give rewriting logic foundations for actors from a somewhat diMerent viewpoint. The paper [53] shows how, for object-oriented modules satisfying some simple requirements, their initial model semantics coincides with a very natural truly concurrent semantics based on a partial order of events. One important strength of the object-oriented viewpoint is that all kinds of entities in the external world can be conceptualized as objects and can be interacted with from a computation by message passing. Built-in objects extend Maude with interfaces allowing interaction with external entities such as internet sockets, $le systems, window systems, and so on. In this way, the computation can be connected with the external world and with other Maude computations in diMerent machines in a distributed way. Interfaces to external entities are speci$ed by means of built-in object-oriented modules de$ning built-in objects. Such built-in object-oriented modules can be imported by ordinary object-oriented modules so that, in general, the object-oriented state of a computation consists of two parts: a con$guration of ordinary objects and messages that is represented in Maude as a multiset of terms representing such objects and messages, and a set of built-in objects, together with messages to and from those objects. Conceptually we can think of these two parts as a single bigger con$guration of objects and messages. However, built-in objects are not themselves visible in the con$guration of ordinary objects and messages, except indirectly, through the messages that they send. In particular, the internal structure of built-in objects is hidden, so that they can only be interacted with by asynchronous message passing. 4. Module operations and parameterized programming Speci$cations and code should be structured in modules of relatively small size to facilitate understandability of large systems, increase reusability of components, and localize the eMects of system changes. Maude fully supports these goals by means of a rich and extensible module algebra supporting, in particular, parameterized programming techniques in the OBJ3 style [37]. Moreover, Maude provides useful basic support for modularity by allowing the de$nition of module hierarchies, that is, acyclic graphs of module importations. Parameterized modules, theories, and views are the basic building blocks of parameterized programming [10,37,26,23]. As in OBJ, a theory 5de$nes the interface of a parameterized module, that is, the structure and properties required of an actual parameter. The instantiation of the formal parameters of a parameterized module with actual parameter modules requires a view from the formal interface theory to the corresponding actual module. That is, views provide the interpretation of the actual parameters. For more details on parameterized modules in Maude, the reader is advised to consult [27]. 4.1. Module hierarchies Mathematically, we can think of module hierarchies as partial orders of rewrite theory inclusions, that is, the theory of the importing module contains the theories of its submodules as subtheories. Recall that a rewrite theory is a four-tuple R=(; E; L; R), where (; E) is a theory in membership equational logic. As already explained in Section 3.2, a system module is a rewrite theory with initial semantics. Note that we can use the inclusion of membership equational logic into rewriting logic to view a functional module specifying an equational theory (; E) as a degenerate case of a rewrite theory, namely the rewrite theory (; E; ∅;∅). In fact the initial algebra of (; E) and the initial model of (; E; ∅;∅) coincide [43]. Therefore, in essence we can view all modules as rewrite theories. The most general form of module inclusion is provided by the including keyword, followed by the name of the imported module. The protecting keyword is a more restricted form of inclusion, in the sense that it makes a semantic assertion about the relationship between the initial models of the two theories. Let R=(; E; L; R)bethe rewrite theory speci$ed by a system module, and let R=(;E;L ;R ) be the theory of a supermodule, so that we have a theory inclusion R⊆R. Then, we can view each model Mof Ras a model M|Rof R, simply by disregarding the extra sorts, operators, equations, membership axioms, and rules in R−R. Since, as explained in Section 3.2, the rewrite theories Rand Rhave respective initial models T Rand T R, by initiality of T Rwe always have a unique R-homomorphism h:T R→T R|R. In the models of a rewrite theory the sorts are interpreted as categories. Then, the protecting importation asserts that for each sort sin the signature of Rthe function hsis an isomorphism of categories. Intuitively, this means that the initial model of the supermodule does not add any “junk” or any “confusion” to the initial model of the submodule. Note that the expected condition would have been to require hto be an R-isomorphism. However, due to the presence of error elements at the kind level, the isomorphism condition would be too strong, since in general, when enlarging 5The reader should be careful in not confusing the diMerent uses of the word “theory” in this section. a signature, there will be new error terms that cannot be proved equal to old ones. See [9] for a detailed discussion of, and proof techniques for, protecting extensions in membership equational logic. Of course, the protecting assertion cannot be checked by Maude at runtime. It requires inductive theorem proving. Using the proof techniques in [9] together with an inductive theorem prover for membership equational logic and a Church–Rosser checker such as those described in [17], this can be done for functional modules; and it seems natural to expect that these techniques and tools will extend to similar ones for rewrite theories. By contrast, the including assertion does not make such requirements on h. It does, however, make some requirements. Namely, if the subtheory Rdoes itself contain a proper subtheory R0that it imports in protecting mode, then the inclusion R0⊆R is still assumed to be protecting. For such an inclusion to become an including assertion, we have to say so by explicitly listing the module de$ning R0in the list of modules imported in including mode. 4.2. Theories Theories are used to declare module interfaces, namely the syntactic and semantic properties to be satis$ed by the actual parameter modules used in an instantiation. As for modules, Maude supports three diMerent types of theories: functional theories, system theories, and object-oriented theories. Their structure is the same as that of their module counterparts. Theories are rewriting logic theories with a loose interpretation, as opposed to modules that have an initial semantics. Therefore, theories are allowed to contain more general sentences that need not satisfy all the requirements described for modules. Let us begin by introducing the functional theory TRIV, which requires just a sort. fth TRIV is sort Elt . endfth The theory of partially ordered sets with an antire:exive and transitive binary operator is expressed in the following way. 6 fth POSET is protecting BOOL . sort Elt . op _<_ : Elt Elt -> Bool . varsXYZ:Elt. eqX<X=false . ceqX<Z=true ifX<YandY<Z. endfth 6As with modules, theories implicitly import the prede$ned module BOOL, and therefore the protecting BOOL declaration is unnecessary. The theory of totally ordered sets, that is, posets in which all pairs of distinct elements have to be related, is speci$ed as follows: fth TOSET is including POSET . varsXY:Elt. eqX<YorY<XorX==Y=true . endfth The including importation of a theory into another theory keeps its loose semantics. However, if the imported theory contains a module, which therefore must be interpreted with an initial semantics, 7then that initial semantics is maintained by the importation. For example, in the de$nition of the POSET theory, the declaration protecting BOOL ensures that the initial semantics of the functional module for the Booleans is preserved, which is in fact a crucial requirement. This requirement is then preserved by TOSET when POSET is included. 4.3. Parameterized modules Theories are used to declare the interface requirements for parameterized modules. Modules can be parameterized by one or more theories. All theories appearing in the interface must be labelled in such a way that their sorts can be uniquely identi$ed. The general form for the interface of a parameterized module is (X1:: T1,::: ,Xn :: Tn)where X1;:::;X nare the labels and T1;:::;T nare the names of the respective parameter theories. All the sorts coming from theories in the interface must be quali$ed by their labels, even if there is no ambiguity. If Zis the label of a parameter theory T, then each sort Sin Thas to be quali$ed as Z.S(the reason for this will be explained below). Moreover, there cannot be subsort overloading between an operator declared in a theory being used as parameter of a parameterized module and an operator declared in the body of the parameterized module, or between operators declared in two parameter theories of the same module. In the body of a parameterized module M(X1:: T1,:::,Xn:: Tn), any parameterized sort Sis written in the form S(X1,:::,Xn). When the module is instantiated with views V1;:::;V nthen this sort becomes S(V1,:::,Vn). Thus, a simple parameterized module for lists is de$ned as follows: fmod LIST(X :: TRIV) is sort List(X) . subsort X.Elt < List(X) . op nil : -> List(X) [ctor] . op __ : List(X) List(X) -> List(X) [ctor assoc id: nil] . endfm 7In Maude, the importation of a module into a theory is supported only in protecting mode. The module LIST has only one parameter. In general, as already mentioned, parameterized modules can have several parameters. It can furthermore happen that several parameters are declared with the same parameter theory. Therefore, parameters cannot be treated as normal submodules, since we do not want them to be shared when their labels are diMerent. We regard the relationship between the body of a parameterized module and the interface of its parameters not as an inclusion, but as a module constructor which is evaluated generating renamed copies of the parameters, which are then included. In such copies of parameter theories sorts are renamed as follows: If Zis the label of a parameter theory T, then each sort Sin Tis renamed to Z.S. This is the reason why all occurrences of these sorts in the body of the parameterized module must mention their corresponding renaming, as explained before. Let us consider as an example the following module TUPLE[2]. Notice the use of the quali$cations for the sorts coming from each of the parameters, and notice also the form of the sort Tuple(C1, C2). fmod TUPLE[2](C1 :: TRIV, C2 :: TRIV) is sort Tuple(C1, C2) . op ((_,_)) : C1.Elt C2.Elt -> Tuple(C1, C2) [ctor] . op p1_ : Tuple(C1, C2) -> C1.Elt . op p2_ : Tuple(C1, C2) -> C2.Elt . var E1 : C1.Elt . var E2 : C2.Elt . eq p1 (E1, E2) = E1 . eq p2 (E1, E2) = E2 . endfm In Maude, the module expression TUPLE[n], for na nonzero natural number, generates a parameterized module specifying a tuple of the corresponding size. For example, for nequal to 2, the system generates automatically the parameterized module TUPLE[2] given above. 4.4. Views Views are used to assert how a particular target module or theory is claimed to satisfy a source theory. In general, there may be several ways in which such requirements might be satis$ed, if at all, by the target module or theory; that is, there can be many diMerent views, each specifying a particular interpretation of the source theory in the target. Each view declaration has an associated set of proof obligations, namely, for each axiom in the source theory it should be the case that the axiom’s translation by the view holds in the target. Since the target can be a module interpreted initially, verifying such proof obligations may in general require inductive proof techniques of the style supported for Maude’s logic in [17]. All views have to be de$ned explicitly, and all of them must have a name. As any theory or module, views should have been de$ned before they are used. In the op fmod_is_sorts_.____endfm:Qid ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet EquationSet -> FModule [ctor] . op mod_is_sorts_._____endm:Qid ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet -> Module [ctor] . Without going into all the syntactic details, we show only the operators used to represent conditions, equations, and rules. sorts EqCondition Condition . subsort EqCondition < Condition . ops (_=_) (_:=_) : Term Term -> EqCondition [ctor] . op _:_ : Term Sort -> EqCondition [ctor] . op _=>_ : Term Term -> Condition [ctor] . op _/\_ : EqCondition EqCondition -> EqCondition [ctor assoc] . op _/\_ : Condition Condition -> Condition [ctor assoc] . sorts Equation EquationSet . subsort Equation < EquationSet . op eq_=_. : Term Term -> Equation [ctor] . op ceq_=_if_. : Term Term EqCondition -> Equation [ctor] . op none : -> EquationSet [ctor] . op __ : EquationSet EquationSet -> EquationSet [ctor assoc comm id: none] . sorts Rule RuleSet . subsort Rule < RuleSet . op rl[_]:_=>_. : Qid Term Term -> Rule [ctor] . op crl[_]:_=>_if_. : Qid Term Term Condition -> Rule [ctor] . op none : -> RuleSet [ctor] . op __ : RuleSet RuleSet -> RuleSet [ctor assoc comm id: none] . As a simple example, the metarepresentation of the module on the left is the term displayed on the right, so that the reader can appreciate the similarity between both notations: fmod NAT is fmod ’NAT is nil sorts Zero Nat . sorts ’Zero ; ’Nat . subsort Zero < Nat . subsort ’Zero < ’Nat . op0:->Zero [ctor] . op ’0 : nil -> ’Zero [ctor] . op s_ : Nat -> Nat [ctor] . op ’s_ : ’Nat -> ’Nat [ctor] . op _+_ : Nat Nat -> Nat op ’_+_ : ’Nat ’Nat -> ’Nat [comm] . [comm] . varsNM:Nat. none eq0+N=N. eq’_+_[’0.Nat, ’N:Nat] = ’N:Nat . eq(sN)+M=s(N+M). eq’_+_[’s_[’N:Nat], ’M:Nat] = ’s_[’_+_[’N:Nat, ’M:Nat]] . endfm endfm Since NAT has no list of imported submodules and no membership axioms, those $elds are $lled, respectively, with the constants nil of sort ImportList, and none of sort MembAxSet. Note that terms of sort Module can be metarepresented again, yielding then a term of sort Term, and this can be iterated an arbitrary number of times. This is in fact necessary when a metalevel computation has to operate at higher levels. A good example is the inductive theorem prover described in [17], where modules are metarepresented as terms of sort Module in the inference rules for induction, but they have to be meta-metarepresented as terms of sort Term when used in strategies that control the application of the inductive inference rules. 5.5. Descent functions The module META-LEVEL has several built-in descent functions that provide useful and eFcient ways of reducing metalevel computations to object-level ones. The operation metaReduce takes as arguments the representation of a module R and the representation of a term tin that module. op metaReduce : Module Term -> [ResultPair] . op {_,_} : Term Type -> ResultPair [ctor] . It returns the representation of the fully reduced form of the term tusing the equations in R, together with its corresponding sort or kind. The interpreter function for metaReduce(S R;S t) rewrites the term tto normal form using only the equations in R, and does so according to the operator evaluation strategies (see the end of Section 2.2 and [33]) declared for each operator in the signature of R, which by default is bottom-up for operators with no such strategies declared. In other words, the interpreter strategy for this function coincides with that of the reduce command in Maude, that is, metaReduce(S R;S t)=IMaude(R;t;reduce): The operation metaRewrite has syntax op metaRewrite : Module Term MachineInt -> [ResultPair] . It is entirely analogous to metaReduce, but instead of using only the equational part of a module it now uses both the equations and the rules to rewrite the term using Maude’s default strategy. Its $rst two arguments are the representations of a module Rand of a term t, and its third argument is a natural number n. Its result is the representation of the term obtained from tafter at most napplications of the rules in Rusing the strategy of Maude’s default interpreter, which applies the rules in a top-down rule fair way. When the value 0 is given as the third argument, no bound is given to the number of rewrites, and rewriting proceeds to the bitter end. Again, metaRewrite is a paradigmatic example of a descent function; its corresponding interpreter strategy is that of the rewrite command in Maude, that is, metaRewrite(S R;S t;n)=IMaude(R;t;rewrite [n]): The operation metaApply has syntax: op metaApply : Module Term Qid Substitution MachineInt -> [ResultTriple] . The $rst four arguments are representations in META-LEVEL of a module R, a term t in R, a label lof some rules in R, and a set of assignments (possibly empty) de$ning a partial substitution for the variables in those rules. The last argument is a natural number nused to enumerate all possible matches (due to the presence of structural axioms for operators or several rules with the same label l). metaApply then returns a triple of sort ResultTriple consisting of a term, with the corresponding sort or kind, and a substitution. The syntax for substitutions and for results is subsort Assignment < Substitution . op _<-_ : Qid Term -> Assignment [ctor] . op none : -> Substitution [ctor] . op _;_ : Substitution Substitution -> Substitution [ctor assoc comm id: none] . op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] . The operation metaApply is evaluated as follows: (1) the term tis $rst fully reduced using the equations in R; (2) the resulting term is matched against all rules with label lpartially instantiated with , with matches that fail to satisfy the condition of their rule discarded; (3) the $rst nsuccessful matches are discarded; if there is an (n+ 1)th match, its rule is applied using that match and the steps 4 and 5 below are taken; otherwise an error is returned; (4) the term resulting from applying the given rule with the (n+ 1)th match is fully reduced using the equations in R; (5) the triple formed using the constructor {_,_,_} whose $rst element is the representation of the resulting fully reduced term, whose second element is the representation of the corresponding type, and whose third element is the representation of the match used in the reduction is returned. The interpreter strategy associated to metaApply(S R;S t; S l; S; n) is not that of a userlevel command in the Maude interpreter. It is instead a built-in strategy internal to the interpreter that attempts one rewrite at the top as explained above. The operation metaXapply, with syntax op metaXapply : Module Term Qid Substitution MachineInt MachineInt MachineInt -> [Result4Tuple] . op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple [ctor] . works as metaApply but using matching with extension (see [15, Section 5:8]) and in any possible position, not only at the top. The $rst two integer arguments indicate, respectively, the minimum and maximum depth in the :attened term (with respect to its associative or associative–commutative operators) where the application of the rule can take place. The last integer argument enumerates the solutions, since there can be diMerent such rewrites with diMerent substitutions and at diMerent positions. The result has an additional component, giving the context inside the given term, where the rewriting has taken place. Contexts (terms with a single “hole”) are de$ned as follows: 8 subsort Context < CTermList . subsorts TermList CTermList < GTermList . op [] : -> Context [ctor] . op _,_ : TermList CTermList -> CTermList [ctor assoc] . op _,_ : CTermList TermList -> CTermList [ctor assoc] . op _[_] : Qid CTermList -> Context [ctor] . The function metaMatch intuitively tries to match at the top two given terms in a module. The last argument is used to enumerate possible matches. If the matching attempt is successful, the result is the corresponding substitution. The generalization to metaXmatch is analogous to the generalization to metaXapply. op metaMatch : Module Term Term MachineInt -> [Substitution]. op metaXmatch : Module Term Term MachineInt MachineInt MachineInt -> [MatchPair] . op {_,_} : Substitution Context -> MatchPair [ctor] . 5.6. Parsing;pretty printing;and sort functions Besides the descent functions already discussed, META-LEVEL provides several other functions that naturally belong to the universal theory and could have been equationally axiomatized in such a theory. However, for eFciency reasons they are provided as builtin functions. These functions allow parsing and pretty printing a term in a module at the metalevel, and performing eFciently a number of useful operations on the sorts declared in a module’s signature. The function metaParse takes as arguments the representation of a module, the representation of a list of tokens as a list of quoted identi$ers, and, optionally, a sort or kind. It returns the metarepresentation of the parsed term of that list of tokens for the signature of the module, which is assumed to be unambiguous. The function metaPrettyPrint takes as arguments the representation of a module Mand the representation of a term t. It returns a list of quoted identi$ers that encode the string of tokens produced by pretty printing tin the syntax given by M.Inthe event of an error an empty list is returned. 8Sort CTermList represents lists of terms with exactly a “hole” in the whole list, and sort GTermList is only needed for the assoc attribute, which is necessary, to make sense. The operations on sorts provide commonly needed functions on the poset of sorts of a module in a built-in way at the metalevel. For example, the function leastSort takes as arguments the representations of a module and a term and computes the (representation of the) least sort of that term in the module, while the Boolean expression sameKind( S M,Ss,s)is true if and only if the sorts sand sbelong to the same kind in the module M. 5.7. Extensions of META-LEVEL In metalevel computations it is very convenient to be able to refer by name to the metarepresentations of modules already entered into the system. To make this possible, Maude allows importation declarations of the form protecting META-LEVEL(M1;:::;M n): where M1;:::;M nis a list of names of user-de$ned modules. With this declaration, new constants M1;:::;M nof sort Module are declared, and new equations making each constant Miequal to the metalevel representation of the module with name Mi(declared previously by the user) are added, for i=1:::n. Thus, after entering the module NAT in Section 5.4 above, we can declare a module that protects META-LEVEL(NAT) and de$nes a function to extract the set of operator declarations of a functional module as follows: fmod META-NAT is protecting META-LEVEL(NAT) . op getOpDeclSet : FModule -> OpDeclSet . var QI : Qid . var IL : ImportList . var SS : QidSet . var SSDS : SubsortDeclSet . var ODS : OpDeclSet . var MAS : MembAxSet . var EqS : EquationSet . eq getOpDeclSet(fmod QI is IL sorts SS . SSDS ODS MAS EqS endfm) = ODS . endfm Then we can apply this function to the constant NAT, which in META-NAT has been declared to be equal to the metarepresentation of the user-de$ned module NAT,as follows: Maude> red getOpDeclSet(NAT) . Result OpDeclSet : op ’0 : nil -> ’Zero [ctor] . op ’s_ : ’Nat -> ’Nat [ctor] . op ’_+_ : ’Nat ’Nat -> ’Nat [comm] . In Maude, we can use the up function to avoid the cumbersome task of explicitly writing the metarepresentation of a term or of a module. For example, to obtain the metarepresentation of the term s0in the module NAT, mathematically denoted s0, we can write Maude> red up(NAT, s 0) . Result Term : ’s_[’0.Nat] Note that the module name is the $rst argument of the up function, with the term of that module to be metarepresented as the second argument. Since the same term can be parsed in diMerent ways in diMerent modules, and therefore can have diMerent metarepresentations depending on the module in which it is considered, the module to which the term belongs has to be used to obtain the correct metarepresentation. Note also that the above reduction only makes sense at the metalevel, that is, in a module importing the module META-LEVEL. Moreover, by evaluating in any module importing the module META-LEVEL the up function with the name of any previously declared module as argument, we obtain the metarepresentation of such a module. The result of a metalevel computation that may use several levels of re:ection can be a term or module metarepresented one or more times, which may be hard to read. To display the output in a more readable form we can use the down command, which is in a sense inverse to up, since it gives us back the term from its metarepresentation. The down command takes two arguments. The $rst argument is the name of the module to which the term to be returned belongs. The metarepresentation of the desired output term should be the result of the command given as second argument. Thus, we can give the following command: Maude> down NAT : red-in META-NAT : metaReduce(NAT, up(NAT,0+s0)). Result Nat:s0 The use of up and down can be iterated with as many levels of re:ection as we wish. 6. Internal strategies As already explained, system modules in Maude are rewrite theories that do not need to be Church–Rosser and terminating. Therefore, we need to have good ways of controlling the rewriting inference process — which in principle could not terminate or could go in many undesired directions — by means of adequate strategies. This need has been addressed in other languages; for example, the ELAN language provides a strategy language to guide the rewrites and allows user extensions for such a language [4–6]. In Maude, thanks to its re:ective capabilities, strategies are made internal to the logic, that is, they are de$ned by rewrite rules in a normal module in Maude, and can be reasoned about as with rules in any other module. In fact, there is great freedom for de$ning many diMerent types of strategies, or even many diMerent strategy languages inside Maude. This can be done in a completely userde$nable way, so that users are not limited by a $xed and closed particular strategy language. A general methodology for de$ning internal strategy languages for re:ective logics is introduced in [12]. In general, strategies for controlling the application of the rules are de$ned by using metaReduce,metaApply, etc., as building blocks, which are then combined to obtain more complex strategies. Let us illustrate some of the possibilities with some strategies controlling the execution of the rule labelled switch in the following module SWITCH.9 mod SWITCH is protecting ARRAY(Int) . varsIJXY:MachineInt . var L : List(Tuple(Int, Int)) . crl [switch] : (I, X) L (J, Y) => (I, Y) L (J, X) if (I, X) L (J, Y) : NeArray(Int) . endm The switch rule rewrites a term of sort Array(Int) in the module ARRAY(Int) to another term in which two of the elements in it have been interchanged. Note that the condition in the rule ensures that it is only applied to valid integer arrays, resulting in another valid integer array; however, this rule is diMerent from the rule sort in Sections 3.2 and 4.5, because it does not check whether the elements are out of place or not. The system thus described is highly concurrent, because the switch rule may be applied concurrently to many diMerent positions in an array. Moreover, this rule gives rise to nondeterministic and nonterminating computations, and therefore we need to control by means of strategies the way in which it is applied. Let us begin by illustrating the use of metaApply for rewriting a term of sort Array(Int) by applying the rule switch once at the top of the term without any speci$c substitution (argument none representing the empty substitution) and using the $rst possible match (last argument 0). The operation getTerm is the selector extracting the $rst component from either a pair of sort ResultPair or a triple of sort ResultTriple (see Section 5.5). Maude> red getTerm(metaApply(SWITCH, (1, 5)(2, 4)(3, 3)), ’switch, none, 0)) . result Term : (1, 3)(2, 4)(3, 5) This simple application of the rule does not have much interest by itself, but shows how it can be used for building more interesting strategies. For example, in this case we see how an array can be rewritten in several diMerent ways, even considering a single rule and rewriting only at the top of the term. The function findAllRews in the module ALL-ONE-STEP-REWRITES below $nds all possible one-step rewrites of a 9The reader should compare this module with the modules INT-SORTING in Section 3.2 and SORTING(X :: TOSET) in Section 4.5. In particular, the imported module ARRAY(Int) is obtained as an instantiation of the parameterized module ARRAY(X) in Section 4.5, and is equivalent to the module INT-ARRAY discussed in Section 2.3. term using a given rule. More precisely, findAllRews(M,T,L), with Ma term of sort Module,Ta term of sort Term metarepresenting a term of a sort in the module metarepresented by M, and Lthe label of a rule in M, returns the set of terms resulting from the application of the rule Lin all possible diMerent ways on term Tin Mby using metaXapply.10 fmod SET(X :: TRIV) is sort Set(X) . subsort X.Elt < Set(X) . op mt : -> Set(X) [ctor] . op _&_ : Set(X) Set(X) -> Set(X) [ctor assoc comm id: mt] . var E : X.Elt . eqE&E=E. endfm view Term from TRIV to META-LEVEL is sort Elt to Term . endv fmod ALL-ONE-STEP-REWRITES is protecting SET(Term) . op findAllRews : Module Term Qid -> Set(Term) . op findAllRewsAux : Module Term Qid MachineInt -> Set(Term) . var T : Term . var M : Module . var L : Qid . var N : MachineInt . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) & findAllRewsAux(M, T, L,N+1) else mt fi . endfm A call to function findAllRews with the metarepresentations of the SWITCH module, of an array, and of the rule label switch gives back all the terms resulting from the 10 The constant maxMachineInt is the largest integer in a given Maude implementation. It is guaranteed (due to virtual memory=address space limitations) that in a nondistributed implementation of Maude a term of depth greater than maxMachineInt cannot be built without running out of swap space. application of such a rule in all possible ways on the term. Maude> red findAllRews(SWITCH;(1, 5)(2, 4)(3, 3);switch) . result Set(Term) : (1, 3)(2, 4)(3, 5) & (1, 4)(2, 5)(3, 3) & (1, 5)(2, 3)(3, 4) It is easy to extend this speci$cation in order to get not only the one-step rewrites, but also to get all rewrites, perhaps up to a given depth, and not only by the application of a single rule, but by considering any rule in a given module. We can even carry on some kind of model checking analysis. This is precisely the idea used by Denker, Meseguer, and Talcott in [21] for analyzing diMerent communication protocols by means of exhaustive execution strategies that achieve a form of model checking analysis of the state space. Another way of controlling the application of the rules consists in choosing some of the possible rewriting paths that can be followed by the application of the rules to a term. For example, we can consider diMerent strategies for the controlled application of the rule switch above for sorting integer arrays. In this case, such strategies correspond to the speci$cation of diMerent sorting algorithms guiding where the switch rule should be applied at each point of the computation. In the module INSERT-STRATEGY below, we give a strategy for sorting integer arrays by following the insertion sort algorithm. This strategy consists in partitioning the array in two regions: a $rst part which is sorted, and a second one which is unsorted. Initially, the entire array is unsorted, and, at each step, the strategy takes the $rst element of the unsorted part and places it into its correct position in the sorted region. This insertion requires the shifting of elements to make room for the element being inserted. The function insert takes a term metarepresenting the nonempty array to be sorted, and calls an auxiliary function, named insertAux, which takes in addition the positions of the $rst and last elements of the array. Its second and third arguments are indexes used to refer to particular elements in the array. More precisely, the second argument represents the position of the $rst element in the unsorted region, that is, the element to be inserted next, and the third argument is used to go through the sorted region looking for the correct position for such an item. The function metaReduce is used for reducing several expressions at the metalevel. For example, the term Tbeing rewritten is used in insert for computing the range of the positions of the array, which are passed as arguments in the initial call to the insertAux function, or for evaluating the Boolean condition in which two elements in diMerent positions are compared in order to decide whether it is worth to interchange them or not. Note the form of the arguments of metaReduce in these calls. We use a combination of the overline notation with the actual metarepresentation of a term in order to simplify the text of the speci$cation as much as possible. For example, the term ’+ [’low[T], S 1] is a simpli$ed representation of the term ’ + [’low[T], ’1. MachineInt], where Tis a variable of sort Term with value the metarepresentation of an array. Such a term is the metarepresentation of low(A)+1, with Athe array metarepresented by T, which is used for calculating the successor of the $rst position of the array being sorted. The function metaXapply is called with an explicit substitution as its fourth argument in order to appropriately instantiate the variables Iand Jused in the switch rule, corresponding to the positions whose values must be interchanged. fmod INSERT-STRATEGY is protecting META-LEVEL(SWITCH) . op insert : Term -> Term . op insertAux : Term Term Term Term Term -> Term . varsTK1K2LH:Term . eq insert(T) = insertAux(T, ’ + [’low[T],S 1], ’ + [’low[T],S 1], ’low[T], ’high[T]) . eq insertAux(T, K2, K1, L, H) = if getTerm(metaReduce(SWITCH, ’ > [K1, L])) == true then if getTerm( metaReduce(SWITCH, ’> [’ ‘[ ‘][T, ’ - [K1,S 1]], ’ ‘[ ‘][T, K1]])) =/= true then insertAux(T, K2, ’ -[K1, S 1], L, H) else insertAux( getTerm( metaXapply(SWITCH, T, ’switch, ((’J:MachineInt <- getTerm(metaReduce(SWITCH, K1))); (’I:MachineInt <- getTerm(metaReduce(SWITCH, ’ - [K1, S 1])))), 0, maxMachineInt, 0)), K2, ’ - [K1, S 1], L, H) fi else if getTerm(metaReduce(SWITCH, ’ < [K2, H])) == true then insertAux(T, ’ + [K2, S 1], ’ + [K2, S 1], L, H) else T fi fi . endfm Notice that, although the rule switch in module SWITCH gives rise to nondeterministic and nonterminating computations, its controlled application by means of the strategy Real-Time Maude. Based on a notion of real-time rewrite theory that can naturally represent many existing models of real-time and hybrid systems, and that has a straightforward translation into an ordinary rewrite theory [58,56], W Olveczky and Meseguer have developed an execution and analysis environment for speci$cations of real-time and hybrid systems called Real-Time Maude [57]. This tool translates realtime rewrite theories into Maude modules and can execute and analyze such theories by means of a library of strategies that can be easily extended by the user to perform other kinds of formal analysis. 8.2. Applications In general, the applications of Maude exploit the good features of rewriting logic as a semantic framework and as a logical framework. Often, they use in a crucial way Maude’s re:ective capabilities. A detailed discussion of diMerent applications is beyond the scope of this paper; we refer the reader to [47,49,50,51,18,21] for recent accounts. As already explained in Section 8.1, an important class of logical framework applications are formal metatool applications that use Maude to generate other formal tools [18]. Semantic framework applications span a wide range of levels, including: formal speci$cation of architectural description languages, object-oriented designs, and distributed middleware [49,50]; formal speci$cation and analysis of network systems and communication protocols [21,50]; and speci$cation and programming of agent and mobile systems (see [50,29] and Section 8.3). Of course, given the high performance of the implementation, Maude is also an attractive very high-level language for a number of programming applications. As explained below, we expect Mobile Maude to further extend the range of such applications. 8.3. Mobile Maude Maude can be used not only for specifying communication systems, but also for programming them. We are currently advancing the design of Mobile Maude [29]. This is an extension of Maude supporting mobile computation that uses re:ection in a systematic way to obtain a simple and general declarative mobile language design. The two key notions are processes and mobile objects. Processes are located computational environments where mobile objects can reside. Mobile objects can move between different processes in diMerent locations, and can communicate asynchronously with each other by means of messages. Each mobile object contains its own code — that is a rewrite theory R— metarepresented as a term S R. In this way, re:ection endows mobile objects with powerful “higher-order” capabilities within a simple $rst-order framework. We expect that Mobile Maude will have good support for secure mobile computation for two reasons. Firstly, mobile objects will communicate with each other and will move from one location to another using state-of-the-art encryption mechanisms. Secondly, because of the logical basis of Mobile Maude, we expect to be able to prove critical properties of applications developed in it with much less eMort than what it would be required if the same applications were developed in a conventional language such as Java. 9. Maude versions: past, present, and future As explained in the introduction, this paper has presented all the main Maude concepts in a version-independent way, without pointing out for each language feature in which version it was introduced. Table 1summarizes this information, and also distinguishes at the same time between the Core Maude features, and the additional features provided in Full Maude. Version 1 of Maude was released in January 1999, while Version 2 was designed in the summer of 2000; most of its features are already implemented at the time of writing. The last row in the table summarizes several features that have been discussed as desirable for future versions, but that are not going to be part of the release of Version 2 of Maude. Appendix A. More details of some examples A.1. CCS Syntax fmod ACTION is protecting QID . sorts Label Act . subsorts Qid < Label < Act . op tau : -> Act [ctor] . *** silent action op ~_ : Label -> Label [ctor] . var N : Label . eq~~N=N. endfm fmod PROCESS is protecting ACTION . sorts ProcessId Process . subsorts Qid < ProcessId < Process . op0:->Process [ctor] . *** inaction op _._ : Act Process -> Process [ctor] . *** prefix op _+_ : Process Process -> Process [ctor assoc comm] . *** summation op _|_ : Process Process -> Process [ctor assoc comm] . *** parallel composition op _\_ : Process Label -> Process [ctor] . *** restriction op _[_/_] : Process Label Label -> Process [ctor] . *** relabelling: [b/a] relabels ‘‘a’’ to ‘‘b’’ endfm Table 1 Language features Core Maude Full Maude Version 1 Functional modules Object-oriented modules System modules Parameterized modules Conditions: single equation Theories Module hierarchies Views Re:ection (metalevel) Module renaming Internal strategies Tuples Descent functions    metaReduce metaRewrite metaApply Up=down commands Prede$ned data types    Boolean values quoted identi$ers machine integers Version 2 Explicit use of kinds Parameterized theories New variable syntax Parameterized views General conditions        memberships equations matching equations rewrites View composition More descent functions    metaXapply metaMatch metaXmatch View lifting More prede$ned data types    natural numbers :oating point numbers strings Built-in object-oriented modules, including TCP socket and $le system interfaces Fair rewriting for system and object-oriented modules Rewrite search and LTL model-checking Sublanguage compiler LaTeX pretty printing Future Uni$cation Narrowing Built-in strategy language Foreign language interface User-de$nable lexical syntax GUI support Additional operator attributes Additional compiler support fmod CCS-CONTEXT is protecting PROCESS . sort Context . op _=def_ : ProcessId Process -> Context [ctor] . op nil : -> Context [ctor] . op _&_ : Context Context -> [Context] [ctor assoc comm id: nil] . op _definedIn_ : ProcessId Context -> Bool . op def : ProcessId Context -> [Process] . op not-defined : -> [Process] [ctor] . op context : -> Context . vars X X’ : ProcessId . var P : Process . vars C C’ : Context . cmb (X =def P)&C:Context if not(X definedIn C) . eq X definedIn nil = false . ceq X definedInC=(X==X’)or(XdefinedIn C’) if (X’ =def P) & C’ := C . eq def(X, nil) = not-defined . ceq def(X, C)=Pif(X=def P) & C’ := C . ceq def(X, C) = def(X, C’) if (X’ =def P) & C’ := C /\ X =/= X’ . endfm A.2. Quicksort strategy The following module QUICKSORT-STRATEGY de$nes the quicksort strategy function, which follows the classical quicksort algorithm for sorting. There is an auxiliary function quicksortAux taking two additional arguments, namely the positions of the $rst and last elements to be considered by the function, that is, the limits of the fragment being considered in each call. There is another auxiliary function partition, which takes as pivot the $rst of the elements in the fragment of the array being considered, and returns a pair of terms (of sort Tuple(Term, Term)) which metarepresent, respectively, the resulting array and the position of the pivot element in it, in such a way that all the elements before such a position are smaller than the pivot, and all the elements after it are greater than or equal to the pivot. The position of the pivot in the resulting array is used by the function quicksortAux for making the recursive calls. Thus, given a fragment with $rst position Land last position H, and with Pthe position of the pivot after the call to partition, the recursive calls will be made with fragments L;P−1 and P+1;H. Note that the module expression TUPLE[2](Term, Term) provides a sort Tuple(Term, Term) with constructor (, ), and with projection functions p1 and p2 . fmod QUICKSORT-STRATEGY is protecting META-LEVEL(SWITCH) + TUPLE[2](Term, Term) . op quicksort : Term -> Term . op quicksortAux : Term Term Term -> Term . op partition : Term Term Term Term -> Tuple(Term, Term) . varsTPLH:Term . eq quicksort(T) = quicksortAux(T, ’low[T], ’high[T]) . eq quicksortAux(T, L, H) = if getTerm(metaReduce(SWITCH, ’_>_[L, H])) == true then nil else if getTerm(metaReduce(SWITCH, ’_==_[L, H])) == true then ’‘(_‘,_‘)[ getTerm(metaReduce(SWITCH, ’_‘[_‘][T, L])), L] else ’__[quicksortAux(p1 partition(T, L, ’_+_[L, 1], H), L,’_-_[p2 partition(T, L, ’_+_[L, 1], H), 1]), ’‘(_‘,_‘)[p2 partition(T, L, ’_+_[L, 1], H), ’_‘[_‘][p1 partition(T, L, ’_+_[L, 1], H), p2 partition(T, L, ’_+_[L, 1], H)]], quicksortAux( p1 partition(T, L, ’_+_[L, 1], H), ’_+_[p2 partition(T, L, ’_+_[L, 1], H), 1], H)]] fi fi . eq partition(T, P, L, H) = if getTerm(metaReduce(SWITCH, ’_>_[L, H])) == true then if getTerm(metaReduce(SWITCH, ’_<_[P, H])) == true then (getTerm( *** move the pivot to position H metaXapply(SWITCH, T, ’switch, ((’I:MachineInt <- getTerm(metaReduce(SWITCH, P))); (’J:MachineInt <- getTerm(metaReduce(SWITCH, H)))), 0, maxMachineInt, 0)), H) else (T, P) *** The pivot is the biggest element fi else if getTerm( metaReduce(SWITCH, ’_>_[’_‘[_‘][T, P],’_‘[_‘][T, L]])) == true then *** the element at L is smaller than the pivot partition(T, P, ’_+_[L, 1], H) else if getTerm( metaReduce(SWITCH, ’_<=_[’_‘[_‘][T, P], ’_‘[_‘][T, H]])) == true then *** the element at H is greater than the pivot partition(T, P, L, ’_-_[H, 1]) else partition( getTerm( metaXapply(SWITCH, T, ’switch, ((’I:MachineInt <- getTerm(metaReduce(SWITCH, L))); (’J:MachineInt <- getTerm(metaReduce(SWITCH, H)))), 0, maxMachineInt, 0)), P, ’_+_[L, 1], ’_-_[H, 1]) fi fi fi . endfm Acknowledgements We would like to thank David de Frutos, Miguel Palomino, Alberto Verdejo, and the anonymous referees for all their helpful comments to previous versions of this paper. References [1] E. Astesiano, H.-J. Kreowski, B. Krieg-BrW uckner (Eds.), Algebraic Foundations of Systems Speci$cation, IFIP State-of-the-Art Reports, Springer, Berlin, 1999. [2] D. Basin, M. Cavel, J. Meseguer, Rewriting logic as a metalogical framework, in: S. Kapoor, S. Prasad (Eds.), Proceedings 20th Conf. on the Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, December 13–15, Lecture Notes in Computer Science, Vol. 1974, Springer, Berlin, 2000, pp. 55–80. [3] J. Bergstra, J. Tucker, Characterization of computable data types by means of a $nite equational speci$cation method, in: J.W. de Bakker, J. van Leeuwen (Eds.), 7th Colloquium on Automata, Languages and Programming, Noordwijkerhout, The Netherlands, Lecture Notes in Computer Science, Vol. 81, Springer, Berlin, 1980, pp. 76–90. [4] P. Borovansk) y , Le Contrˆole de la R)e)ecriture: ) Etude et Implantation d’un Formalisme de Strat)egies. Ph.D. Thesis, Universit)e Henri Poincar)e – Nancy I, October 1998. [5] P. Borovansk) y , C. Kirchner, H. Kirchner, Controlling rewriting by rewriting, in: J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, pp. 168–188, http:==www.elsevier.nl=locate=entcs=volume4.html. [6] P. Borovansk) y , C. Kirchner, H. Kirchner, Rewriting as a uni$ed speci$cation tool for logic and control: the ELAN language, in: M.P.A. Sellink (Ed.), 2nd Int. Workshop on the Theory and Practice of Algebraic Speci$cations, Amsterdam, The Netherlands, September 25–26, 1997, Electronic Workshops in Computing. Springer, Berlin, 1998, http:==www.ewic.org.uk=ewic= workshop=view.cfm=ASFSDF-97. [7] P. Borovansk) y , C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, An overview of ELAN, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 329–344, http:==www.elsevier.nl=locate= entcs/volume15.html. [8] P. Borovansk) y , C. Kirchner, H. Kirchner, P.-E. Moreau, M. Vittek, ELAN: a logical framework based on computational systems, in: J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, pp. 35–50, http:==www.elsevier.nl=locate=entcs=volume4.html. [9] A. Bouhoula, J.-P. Jouannaud, J. Meseguer, Speci$cation and proof in membership equational logic, Theoret. Comput. Sci. 236 (2000) 35–132. [10] R. Burstall, J.A. Goguen, The semantics of Clear, a speci$cation language, in: D. BjHrner (Ed.), Proc. 1979 Copenhagen Winter School on Abstract Software Speci$cation, Lecture Notes in Computer Science, Vol. 86, Springer, Berlin, 1980, pp. 292–332. [11] G. Carabetta, P. Degano, F. Gadducci, CCS semantics via proved transition systems and rewriting logic, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 253–272, http:==www. elsevier.nl=locate=entcs=volume15.html. [12] M. Clavel, Re:ection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications, CSLI Publications, Stanford, CA, 2000. [13] M. Clavel, F. Dur)an, S. Eker, P. Lincoln, N. Mart) 0-Oliet, J. Meseguer, Metalevel computation in Maude, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 3–24, http:==www.elsevier.nl=locate=entcs=volume15.html. [14] M. Clavel, F. Dur)an, S. Eker, P. Lincoln, N. Mart) 0-Oliet, J. Meseguer, J.F. Quesada, Maude: speci$cation and programming in rewriting logic, Manual distributed as documentation of the Maude system, Computer Science Laboratory, SRI International, http:==maude.csl.sri.com=manual, January 1999. [15] M. Clavel, F. Dur)an, S. Eker, P. Lincoln, N. Mart) 0-Oliet, J. Meseguer, J.F. Quesada, A Maude tutorial, Tutorial distributed as documentation of the Maude system, Computer Science Laboratory, SRI International. Presented at the European Joint Conference on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25, 2000, http:==maude.csl.sri.com=tutorial, March 2000. [16] M. Clavel, F. Dur)an, S. Eker, P. Lincoln, N. Mart) 0-Oliet, J. Meseguer, J.F. Quesada, Towards Maude 2.0, in: K. Futatsugi (Ed.), Proc. 3rd Int. Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, Electronic Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2000, pp. 297–318, http:==www. elsevier.nl=locate=entcs=volume36.html. [17] M. Clavel, F. Dur)an, S. Eker, J. Meseguer, Building equational proving tools by re:ection in rewriting logic, in: Proc. CafeOBJ Symp. ’98, Numazu, Japan, CafeOBJ Project, April 1998, http:==maude.csl.sri.com=papers. [18] M. Clavel, F. Dur)an, S. Eker, J. Meseguer, M.-O. Stehr, Maude as a formal meta-tool, in: J.M. Wing, J. Woodcock, J. Davies (Eds.), Proc. FM’99 — Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20–24, Volume II, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1684–1703. [19] M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, in: J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, pp. 65–89, http:==www.elsevier.nl=locate=entcs=volume4.html. [20] M. Clavel, J. Meseguer, Re:ection in conditional rewriting logic, Theoret. Comput. Sci. 2002, this volume. [21] G. Denker, J. Meseguer, C.L. Talcott, Formal speci$cation and analysis of active networks and communication protocols: the Maude experience, in: D. Maughan, G. Koob, S. Saydjari (Eds.), Proc. DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25–27, 2000, IEEE Computer Society Press, Silver Spring, MD, 2000, pp. 251–265, http:==schafercorp-ballston.com=discex=. [22] N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Chap. 6, The MIT Press=Elsevier, Cambridge, MA, Amsterdam, 1990, pp. 243–320. [23] R. Diaconescu, K. Futatsugi, CafeOBJ Report, The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Speci$cation, AMAST Series in Computing. Vol. 6, World Scienti$c, Singapore, 1998. [24] R. Diaconescu, K. Futatsugi, S. Iida, Component-based algebraic speci$cation and veri$cation in CafeOBJ, in: J.M. Wing, J. Woodcock, J. Davies (Eds.), Proc. FM’99 — Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20–24, Volume II, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1644–1663. [25] R. Diaconescu, K. Futatsugi, M. Ishisone, T. Sawada, A.T. Nakagawa, An overview of CafeOBJ, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 75–88, http:==www.elsevier. nl=locate=entcs=volume15.html. [26] R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularization, in: G. Huet, G. Plotkin, C. Jones (Eds.), Proc. Workshop on Logical Frameworks, Edinburgh, UK, May 1991, Cambridge University Press, Cambridge, May 1991, pp. 83–130. [27] F. Dur)an, A Re:ective Module Algebra with Applications to the Maude Language, Ph.D. Thesis, Universidad de M)alaga, Spain, June 1999, http:==maude.csl.sri.com=papers. [28] F. Dur)an, The extensibility of Maude’s module algebra, in: T. Rus (Ed.), Proc. 8th Int. Conf. on Algebraic Methodology and Software Technology, AMAST 2000, Iowa City, Iowa, USA, May 20–27, 2000, Lecture Notes in Computer Science, Vol. 1816, Springer, Berlin, 2000, pp. 422–437. [29] F. Dur)an, S. Eker, P. Lincoln, J. Meseguer, Principles of mobile Maude, in: D. Kotz, F. Mattern (Eds.), Proc. 2nd Int. Symp. on Agent Systems, Mobile Agents, and Applications, Proc. 4th Int. Symp. on Mobile Agents, ASA=MA 2000, Zurich, Switzerland, September 13–15, 2000, Lecture Notes in Computer Science, Vol. 1882, Springer, Berlin, 2000, pp. 73–85. [30] F. Dur)an, J. Meseguer, An extensible module algebra for Maude, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 185–206, http:==www.elsevier.nl=locate=entcs=volume15.html. [31] F. Dur)an, J. Meseguer, Parameterized theories and views in Full Maude 2.0, in: K. Futatsugi (Ed.), Proc. 3rd Int. Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, Electronic Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2000, pp. 319–337, http:==www.elsevier.nl=locate=entcs=volume36.html. [32] S. Eker, Fast matching in combination of regular equational theories, in: J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, pp. 90–108. http:==www.elsevier.nl=locate=entcs=volume4.html. [33] S. Eker, Term rewriting with operator evaluation strategy, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, pp. 45–62. http:==www.elsevier.nl=locate=entcs=volume15.html. [34] K. Futatsugi (Ed.), Proc. 3rd Int. Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, Electronic Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2000, http:==www.elsevier.nl=locate=entcs=volume36.html. [35] F. Gadducci, U. Montanari, Comparing logics for rewriting: rewriting logic, action calculi and tile logic, Theoret. Comput. Sci., 2002, this volume. [36] J.A. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci. 105 (1992) 217–273. [37] J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, J.-P. Jouannaud, Introducing OBJ, in: J.A. Goguen, G. Malcolm (Eds.), Software Engineering with OBJ: Algebraic Sspeci$cation in Action, Advances in Formal Methods, Chap. 1, Kluwer Academic Publishers, Dordrecht, 2000, pp. 3–167. [38] J.-P. Jouannaud, H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput. 15 (1986) 1155–1194. [39] C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-Ya-Mousson, France, September 1–4, 1998, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998, http://www.elsevier.nl/ locate/entcs/volume15.html. [40] C. Kirchner, H. Kirchner, M. Vittek, Designing constraint logic programming languages using computational systems, in: V. Saraswat, P. van Hentenryck (Eds.), Principles and Practice of Constraint Programming: The Newport Papers, The MIT Press, Cambridge, MA, 1995, pp. 133–160. [41] N. Mart) 0-Oliet, J. Meseguer, Rewriting logic as a logical and semantic framework, in: D. Gabbay (Ed.), Handbook of Philosophical Logic, Second Edition, Vol. 9, Kluwer Academic Publishers, Dordrecht, 2002, http:==maude.csl.sri.com=papers. [42] J. Meseguer, Rewriting as a uni$ed model of concurrency, Technical Report SRI-CSL-90-02, SRI International, Computer Science Laboratory, February 1990, Revised June 1990. [43] J. Meseguer, Conditional rewriting logic as a uni$ed model of concurrency, Theoret. Comput. Sci. 96 (1) (1992) 73–155. [44] J. Meseguer, A logical theory of concurrent objects and its realization in the Maude language, in: G. Agha, P. Wegner, A. Yonezawa (Eds.), Research Directions in Concurrent Object-Oriented Programming, The MIT Press, Cambridge, MA, 1993, pp. 314–390. [45] J. Meseguer, Solving the inheritance anomaly in concurrent object-oriented programming, in: O.M. Nierstrasz (Ed.), Proc. 7th European Conf. ECOOP’93 — Object-Oriented Programming, Kaiserslautern, Germany, July 26–30, 1993, Lecture Notes in Computer Science, Vol. 707, Springer, Berlin, 1993, pp. 220–246. [46] J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, http:==www.elsevier.nl=locate=entcs=volume4.html. [47] J. Meseguer, Rewriting logic as a semantic framework for concurrency: a progress report, in: U. Montanari, V. Sassone (Eds.), Proc. 7th Int. Conf. on CONCUR’96: Concurrency Theory, Pisa, Italy, August 26–29, 1996, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996, pp. 331–372. [48] J. Meseguer, Membership algebra as a logical framework for equational speci$cation, in: F. Parisi-Presicce (Ed.), Proc. 12th Int. Workshop on Recent Trends in Algebraic Development Techniques, WADT’97, Tarquinia, Italy, June 3–7, 1997, Selected Papers, Lecture Notes in Computer Science, Vol. 1376, Springer, Berlin, 1998, pp. 18–61. [49] J. Meseguer, Research directions in rewriting logic, in: U. Berger, H. Schwichtenberg (Eds.), Proceedings of the NATO Advanced Study Institute on Computational Logic held in Marktoberdorf, Germany, July 29–August 6, 1997, NATO ASI Series F: Computer and Systems Sciences, Vol. 165, Springer, Berlin, 1998, pp. 347–398. [50] J. Meseguer, Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems, in: S.F. Smith, C.L. Talcott (Eds.), Proc. IFIP Conf. on Formal Methods for Open Object-Based Distributed Systems IV, FMOODS 2000, September 6–8, 2000, Stanford, CA, USA, Kluwer Academic Publishers, Dordrecht, 2000, pp. 89–117. [51] J. Meseguer, Rewriting logic and Maude: concepts and applications, in: L. Bachmair (Ed.), Proc. 11th Int. Conf. on Rewriting Techniques and Applications, RTA 2000, Norwich, UK, July 10–12, 2000, Lecture Notes in Computer Science, Vol. 1833, Springer, Berlin, 2000, pp. 1–26. [52] J. Meseguer, J.A. Goguen, Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems, Inform. Comput. 104 (1) (1993) 114–158. [53] J. Meseguer, C.L. Talcott, A partial order event model for concurrent objects, in: J.C.M. Baeten, S. Mauw (Eds.), Proc. 10th Int. Conf. on CONCUR’99, Concurrency Theory, Eindhoven, The Netherlands, August 24–27, 1999, Lecture Notes in Computer Science, Vol. 1664, Springer, Berlin, 1999, pp. 415–430. [54] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood CliMs, NJ, 1989. [55] T. Nipkow, Combining matching algorithms: the regular case, J. Symbolic Comput. 12 (1991) 633–653. [56] P.C. W Olveczky, Speci$cation and Analysis of Real-Time and Hybrid Systems in Rewriting Logic, Ph.D. Thesis, University of Bergen, Norway, 2000, http:==maude.csl.sri.com=papers. [57] P.C. W Olveczky, J. Meseguer, Real-time Maude: a tool for simulating and analyzing real-time and hybrid systems, in: K. Futatsugi (Ed.), Proc. 3rd Int. Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, Electronic Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2000, pp. 361–383, http:==www.elsevier.nl=locate=entcs=volume36.html. [58] P.C. W Olveczky, J. Meseguer, Speci$cation of real-time and hybrid systems in rewriting logic, Theoret. Comput. Sci., 2002, this volume. [59] J.F. Quesada, The SCP parsing algorithm based on syntactic constraints propagation, Ph.D. Thesis, Universidad de Sevilla, Spain, June 1997. [60] J.F. Quesada, The Maude parser: parsing and meta-parsing 2-extended context-free grammars, Tech. Rep. Computer Science Laboratory, SRI International, 2001, in preparation. [61] T. Suzuki, A. Middeldorp, T. Ida, Level-con:uence of conditional rewrite systems with extra variables in right-hand sides, in: J. Hsiang (Ed.), Proc. 6th Int. Conf on Rewriting Techniques and Applications, RTA’95, Kaiserslautern, Germany, April 5–7, 1995, Lecture Notes in Computer Science, Vol. 914, Springer, Berlin, 1995, pp. 179–193. [62] C.L. Talcott, An actor rewriting theory, in: J. Meseguer (Ed.), Proc. 1st Int. Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, Sept. 1996, pp. 360–383, http:==www.elsevier.nl=locate=entcs=volume4.html. [63] C.L. Talcott, Interaction semantics for components of distributed systems, in: E. Najm, J.-B. Stefani (Eds.), Proc. IFIP Conf. on Formal Methods for Open Object-Based Distributed Systems, FMOODS’96, Chapman & Hall, London, 1997, pp. 154–169. [64] C.L. Talcott, Towards a toolkit for actor system speci$cation, in: T. Rus (Ed.), Proc. 8th Int. Conf on Algebraic Methodology and Software Technology, AMAST 2000, Iowa City, Iowa, USA, May 20–27, 2000, Lecture Notes in Computer Science, Vol. 1816, Springer, Berlin, 2000, pp. 391–406. [65] C.L. Talcott, Actor theories in rewriting logic, Theoret. Comput. Sci., 2002, this volume. [66] A. Verdejo, N. Mart) 0-Oliet, Executing and verifying CCS in Maude, Tech. Rep. 99-00, Departamento de Sistemas Inform)aticos y Programaci)on, Universidad Complutense de Madrid, Feb. 2000, http:==maude.csl.sri.com=casestudies=ccs. [67] P. Viry, Rewriting: an eMective model of concurrency, in: C. Halatsis, D. Maritsas, G. Philokyprou, S. Theodoridis (Eds.), Proc. 6th Int. Conf. on PARLE’94 Parallel Architectures and Languages Europe, PARLE Conference, Athens, Greece, July 4–8, 1994, Lecture Notes in Computer Science, Vol. 817, Springer, Berlin, 1994, pp. 648–660. [68] P. Viry, Rewriting modulo a rewrite system, Technical Report TR-95-20, Dipartimento di Informatica, UniversitYa di Pisa, December 1995, ftp:==ftp.di.unipi.it=pub=techreports=TR-95-20.ps.Z.