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.maudeThe 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 MFE.zip 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:
AProVE is available at http://www-i2.informatik.rwth-aachen.de/AProVE/. The Termination Competition version (for linux) is available here. Use the runme script as executable (modify it as necessary). Download the files aprove.jar and runme in the same directory. A local copy of the aprove.jar file is available here.
MuTerm is available at http://www.dsic.upv.es/~slucas/csr/termination/muterm/. We recommend MuTerm 4.4. The Termination Competition version (for linux) is available here. Use the runme script as executable (modify it as necessary). Download the files muterm, bc2sat, sat, and runme in the same directory.
Downloads |
Files to download:
|
comments
to duran[at]lcc[dot]uma[dot]es
|