MFE - The Maude Formal Environment

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.

How to use the tool

By executing Maude 2.6++ and then loading the MFE.maude file the tool would start showing its banner. 

$ maude mfe.maude
                  --- Welcome to Maude ---
            With CETA extensions
           Maude-ceta 2.6 built: Nov  2 2011 12:54:56
           Copyright 1997-2010 SRI International
                  Tue Feb 21 12:52:39 2012

           Full Maude 2.6c July 22nd 2011

   Inductive Theorem Prover - July 20th 2010
   Sufficient Completeness Checker 2a - August 2010
   Church-Rosser Checker 3l - November 24th 2010
   Coherence Checker 3l - November 24th 2010
   Maude Termination Tool 1.5h January 1st 2011
   Equality Enrichments 0.99 - July 2011


The MFE extends Full Maude, and therefore all the functionality of Full Maude, including all its commands and facilities for loading modules, theories, and views is available in the MFE. Moreover, the MFE provides the following commands:

If the input (between parentheses) entered is not parseable by the MFE, then it is submitted to the currently active tool. In this way, the interaction with each of the tools integrated in the environment remains almost as before the integration. The integration nevertheless suggests the addition of commands 

Additionally, each of the tools would provide its own list of available commands. Use the help command or the tool documentation for further information.   

On the installation of MFE

To install the tool you need to download the 2.6++ version of Maude and the file. Additionally, termination checks using MTT will require the installation of back-end tools, like CiME, AProVE, MuTerm, etc. If they are not properly installed a message of its nonavailability will be given by MFE when trying to complete a check of termination. 

The interaction with the different termination tools is carried out following ideas already in MTT (see additional details). To simplify the installation and its usage, MFE assumes a file with name "mfe.config" in the directory of the Maude 2.6++ executable (or in MAUDE_LIB). See the mfe.config file included in the Maude 2.6++ distribution. This file contains a line per tool with the format 

    <name with which you will refer to the tool inside MFE> <path of the batch of the tool> <extension of the files to load>

For instance, the contains of this text file could be:

    aprove /home/me/Tools/runme .trs
    ttc /home/me/Tools/runmepar

The third parameter is optional. MTT requires Maude and at least on back-end tool to be available in the system:


Files to download:

 comments to duran[at]lcc[dot]uma[dot]es