New evaluation commands for Maude within Full Maude


Francisco Durán, Santiago Escobar, and Salvador Lucas


The reflective capabilities of Maude enable its use as a metalenguage for building language extensions for Maude itself. Full Maude is a meta-level tool aimed at testing and experimenting with new features and capabilities which are not directly present in (Core) Maude yet. In this paper we describe a number of new evaluation commands for Maude written in Full Maude. They give support to the use of Maude strategy annotations as suitable devices for improving termination of Maude programs without lacking correctness and completeness of computations.


Declarative programming, Maude, strategy annotations.