MFE

The Maude Formal Environment (MFE) is an executable and highly extensible software infrastructure within which a user can interact with several tools to mechanically verify properties of Maude specifications. In MFE, tools can interoperate to discharge proof obligations of different nature without switching between different tool environments. The integration of different tools inside MFE’s common environment presents the user with a consistent user interface, a mechanism to keep track of pending proof obligations, and allows the execution of several instances of each tool, among other features. MFE is naturally modeled in Maude as an object-based system in which the tools are objects and their communication mechanism is message passing. User interaction is available through Full Maude, an extension of Maude that has become a common base on top of which tools can be built, offering a modular design for easily integrating other tools written in Maude. Five tools, with highly different designs and implementations, have already been integrated in MFE. Namely, the Maude Termination Tool (MTT), the Church-Rosser Checker (CRC), the Coherence Checker (ChC), the Sufficient Completeness Checker (SCC), and Maude’s Inductive Theorem Prover (ITP). Despite their heterogeneousness and isolated conception, these tools were integrated in MFE with very few code alterations, many of these due to renaming of sorts and operators. For tools which depend on external utilities not directly available from Maude such as MTT and SCC, we have extended the latest release of the Maude system with built-in operators associated with appropriate C++ code that interacts with the external tools. A similar extension was already performed for the SCC.