As in Clear [7], OBJ [27], and other specification languages in that tradition, the abstract syntax for writing specifications in Maude can be seen as given by module expressions, where the notion of module expression is understood as an expression that defines a new module out of previously defined modules by combining and/or modifying them according to a specific set of operations, that is, according to a specific module algebra. In fact, structuring is essential in all specification languages, not only to facilitate the construction of specifications from already existing ones--with more or less flexible reusability mechanisms--but also for managing the complexity of understanding and analyzing large specifications.
A module importing some combination of modules, given by module expressions, can be seen as a structured module with more or less complex relationships among its component submodules. For execution purposes, however, we typically want to convert this structured module into an equivalent unstructured module, that is, into a "flattened" module without submodules. In the case of Maude, this flattened module will then be compiled into the rewrite engine. By systematically using the metaprogramming capabilities of Maude we can both evaluate module expressions into structured module hierarchies, and flatten such hierarchies into unstructured modules for execution. All such module operations are defined by rewrite rules that operate on the metalevel term representations of modules. This is essentially the idea behind the implementation of Full Maude in Maude.
The current version of Full Maude supports two types of module expression: instantiation of a module expression with a view expression, and renaming of a module expression with a set of mappings. The syntax used for both of them is the same one as in OBJ3, namely
op _[_] : ModExp ViewExp -> ModExp .for instantiation of parameterized modules, and
op _*(_) : ModExp MapList -> ModExp .for renamings. As we saw in Section 3.5.2, a view expression can be a single view name, or a sequence of view names separated by commas in case the module being instantiated has several parameters.
Instantiation is the process by which actual parameters are bound to the parameters of a parameterized module and a new module is created as a result. This can be seen in fact as the evaluation of a module expression. The instantiation requires a view from each formal parameter to its corresponding actual parameter. Each such view is then used to bind the names of sorts, operators, etc. in the actual parameters to the corresponding sorts, operators (or expressions), etc. in the target.
The instantiation of a parameterized module has to be made with views explicitly defined previously. Thus, we can have a set of machine integers with the module expression SET[MachineInt], or a pair of machine integers as tosets with TOSET-PAIR[MachIntAsToset, MachIntAsToset].
As mentioned in Section 3.5.3, we can define views from theories to theories. Using such views we can, for example, instantiate the module SET with the view Toset given in the previous section. The result is a module SET[Toset] which is still parameterized, but now by the theory TOSET. We can instantiate it again with a view from TOSET to some other theory or module, for example, MachIntAsToset, obtaining the module SET[Toset][MachIntAsToset], which is just a set of machine integers. For example, we can give a more concise definition of the parameterized module TOSET-PAIR[X::TOSET,Y::TOSET] using these ideas as follows.
(fmod TOSET-PAIR[X :: TOSET, Y :: TOSET] is
protecting PAIR[Toset, Toset][X, Y] .
op _<_ : Pair[Toset, Toset][X, Y] Pair[Toset, Toset][X, Y]
-> Bool .
var A A' : Elt.X .
var B B' : Elt.Y .
eq < A ; B > < < A' ; B' >
= (A < A') or (A == A' and B < B') .
endfm)
Let us consider now the following module MAX, parameterized by the theory TOSET. Given a set of elements in this toset, the function max returns the maximum element in the set.
(fmod MAX[T :: TOSET] is
protecting SET[Toset][T] .
op max : NeSet[Toset][T] -> Elt.T .
var E : Elt.T .
var S : NeSet[Toset][T] .
eq max(E) = E .
ceq max(E S) = E if max(S) < E .
ceq max(E S) = max(S) if not (max(S) < E) .
endfm)
Module expressions can be arguments of a protecting or including importation, or can be used as the module in which to reduce or rewrite by a red or rew command. In general we can use module expressions in any place where the name of a module is expected. In fact, in Full Maude the name of a module is given by a module expression, and each time a new module expression is entered, the module expression is evaluated, and a module is generated with this module expression as its name. It is this module which is passed to the engine to get the intended result.
Let us see how module expressions can be used in red commands using the instantiation of MAX with the view MachIntAsToset presented in Section 3.5.3.
Maude> (red-in MAX[MachIntAsToset] : max(5 4 8 4 6 5) .) Result : 8
Notice that, if we have several parameters, we can instantiate the parameterized module with some views going to theories and others going to modules. The result in this case is the expected one, that is, we get a module parameterized by the targets of those views going to theories.
A renaming can be considered as a function that, given a module M and a list of mappings S, returns a copy of the module in which the names of the sorts, operations, etc. are changed as indicated by the mappings. More precisely, given a structured specification, the renaming not only causes the creation of a copy of the top module in the structure, but renames also the part of the submodule structure that is affected by the renaming. For any other submodule M' in the structure which is affected by the mappings, a renamed copy of it is generated with name M' * (S'), where S' is the subset of mappings in S that affect M'.
The complete syntax for renaming maps is as follows.
op op_to_ : Token Token -> Map . op op_:_->_to_ : Token SortList Sort Token -> Map . op op_: ->_to_ : Token Sort Token -> Map . op op_to_[_] : Token Token AttrList -> Map . op op_:_->_to_[_] : Token SortList Sort Token AttrList -> Map . op op_: ->_to_[_] : Token Sort Token AttrList -> Map . op sort_to_ : Sort Sort -> Map . op label_to_ : Token Token -> Map . op class_to_ : Sort Sort -> Map . op attr_._to_ : Token Sort Token -> Map . op msg_to_ : Token Token -> Map . op msg_:_->_to_ : Token SortList Sort Token -> Map . op msg_: ->_to_ : Token Sort Token -> Map . subsort Map < MapList . op _,_ : MapList MapList -> MapList [assoc prec 42] .Notice that we also allow the renaming of rule labels, which may be useful for metalevel applications.
A set of attributes can also be given in the renaming of an operator. This allows changing syntactic attributes, such as the precedence values and the gathering patterns, which may be of practical relevance when dealing with mixfix syntax. For example, when a change in the syntax of the operator could cause a parsing different from the intended one. Let us see an example in which modifying the grammatical attributes of an operator is useful. Suppose that we want to change the syntax of the function max in the module MAX presented above, to maximum_. We can do the following reduction.
Maude> (red-in MAX[MachIntAsToset]
* (op max : NeSet[Toset][MachIntAsToset]
-> MachineInt to maximum_)
: maximum 5 4 8 4 6 5 .)
Result : 4 5 6 8
This result may seem strange, but makes perfect sense. In fact the system indicates the term that it has reduced:
Reduce in MAX[MachIntAsToset]
* (op max : NeSet[Toset][MachIntAsToset]
-> MachineInt to maximum_)
: (maximum 5) 4 8 4 6 5 .
What has happened is that the precedence given by default to the operator with
this new syntax is the same as that given to the operator __,
and therefore, by the default gathering patterns, this is a valid
parse. Notice that the other elements passed to the function maximum
have "disappeared" by the equations in SET. We can obtain the
intended result by placing parentheses around the set of numbers, but it is
more convenient to change the precedence values of the attributes. We can, for
example, raise the precedence of maximum_.
Maude> (red-in MAX[MachIntAsToset]
* (op max : NeSet[Toset][MachIntAsToset]
-> MachineInt to maximum_
[prec 41])
: maximum 5 4 8 4 6 5 .)
Reduce in MAX[MachIntAsToset]
* (op max : NeSet[Toset][MachIntAsToset]
-> MachineInt to maximum_
[prec 41])
: maximum (5 4 8 4 6 5) .
Result : 8
More examples can be found in Appendix E. We finish this section with an example involving object-oriented modules, namely, a stack of banking accounts.
(view Accnt from CELL to ACCNT is
sort Elt to MachineInt .
class Cell to Accnt .
attr contents . Cell to bal .
endv)
Now we can do the following rewriting.
Maude> (rew-in STACK2[Accnt] :
< 'stack : Stack[Accnt] | first : null >
< 'paul : Accnt | bal : 5000 >
< 'peter : Accnt | bal : 2000 >
< 'mary : Accnt | bal : 15000 >
('stack push 'paul)
('stack push 'peter)
('stack push 'mary)
('stack top 'peter)
('stack pop) .)
Result Configuration : ('peter elt 2000)
< 'stack : Stack[Accnt] |
first : o('stack, 1) >
< 'paul : Accnt | bal : 5000 >
< 'peter : Accnt | bal : 2000 >
< 'mary : Accnt | bal : 15000 >
< o('stack, 0) : Node[Accnt] |
next : null, node : 'peter >
< o('stack, 1) : Node[Accnt] |
next : o('stack, 0), node : 'mary >