System Modules

A Maude system module specifies a rewrite theory. A rewrite theory has sorts, kinds, and operators (perhaps with frozen arguments), and can have three types of statements: equations, memberships, and rules, all of which can be conditional. Therefore, any rewrite theory has an underlying equational theory, containing the equations and memberships, plus the rules. What is the intuitive meaning of such rules? Computationally, they specify local concurrent transitions that can take place in a system if the pattern in the rule's lefthand side matches a fragment of the system state and the rule's condition is satisfied. In that case, the transition specified by the rule can take place, and the matched fragment of the state is transformed into the corresponding instance of the righthand side. Logically, that is, when we use rewriting logic as a logical framework to represent other logics as explained in Section 1.4, a rule specifies a logical inference rule, and rewriting steps therefore represent inference steps.

As was mentioned in Section 3.2, a system module is declared in Maude using the keywords

  mod $\langle$ModuleName$\rangle$ is $\langle$DeclarationsAndStatements$\rangle$ endm

As for functional modules the first bit of information in the specification is the module's name, which must be an identifier. For example,

  mod VENDING-MACHINE is
    ...
  endm

where the dots stand for all the declarations and statements in the module, which can be:

1. module importations,
2. sort and subsort declarations,
3. operator declarations,
4. variable declarations,
5. equation and membership statements, and
6. rule statements.

Since declarations 1-4 and equational statements (5) are exactly as for functional modules, all we have left to explain is how rules (conditional or not) are declared. As for equation and membership statements, rules can be declared with any of the attributes label, metadata, and nonexec (see Section 4.5). However, the owise attribute can only be used with equations.