Reflection

This is a very important feature of Maude. Intuitively, it means that Maude programs can be metarepresented as data, which can then be manipulated and transformed by appropriate functions. It also means that there is a systematic causal connection between Maude modules themselves and their metarepresentations, in the sense that we can either first perform a computation in a module and then metarepresent its result, or, equivalently, we can first metarepresent the module and its initial state and then perform the entire computation at the metalevel. Finally, the metarepresentation process can itself be iterated giving rise to a very useful reflective tower. Thanks to Maude's logical semantics (more on this in Section 1.2), all this is not just some kind of ``glorified hacking,'' but a precise form of logical reflection with a well-defined semantics (see Chapter 11 and [20,21]). There are many important applications of reflection. Let us mention just three:

• Internal strategies. Since the rewrite rules of a system module can be highly nondeterministic, there may be many possible ways in which they can be applied, leading to quite different outcomes. In a distributed object system this may be just part of life: provided some fairness assumptions are respected, any concurrent execution may be acceptable. But what should be done in a sequential execution? Maude does indeed support two different fair execution strategies in a built-in way through its rewrite and frewrite commands (see Section 5.4). But what if we want to use a different strategy for a given application? The answer is that Maude modules can be executed at the metalevel with user-definable internal strategies^1.5 (see Section 11.5). Such internal strategies can be defined by rewrite rules in a metalevel module that guides the possibly nondeterministic application of the rules in the given ``object level'' module. This process can be iterated in the reflective tower. That is, we can define meta-strategies, meta-meta-strategies, and so on.
• Module algebra. The entire module algebra in which parameterized modules can be composed and instantiated becomes expressible within the logic, and extensible by new module operations that transform existing modules metarepresented as data. This is of more than theoretical interest: Maude's module algebra is realized exactly in this way by Full Maude, a Maude program defining all the module operations and easily extensible with new ones (see Part II of this manual).
• Formal tools. The verification tools in Maude's formal environment must take Maude modules as arguments and perform different formal analyses and transformations on such modules. This is again done by reflection in tools such as Maude's inductive theorem prover, the Church-Rosser checker, the Maude termination tool, the Real-Time Maude tool, and so on.