Tool Interoperability in the Maude Formal Environment

Abstract

We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the Church-Rosser Checker, the Coherence Checker, and the Maude Inductive Theorem Prover. We explain the high-level design decisions behind MFE, give a summarized account of its main features, and illustrate with an example the interoperation of the tools available in its current release.

Presentamos Maude Formal Environment (MFE), una especificación formal ejecutable en Maude dentro de la cual un usuario puede interactuar sin problemas con la herramienta de terminación de Maude, el verificador de integridad suficiente de Maude, el verificador de Church-Rosser, el verificador de coherencia y el teorema inductivo de Maude. Tirador de pruebas. Explicamos las decisiones de diseño de alto nivel detrás de MFE, brindamos una descripción resumida de sus características principales e ilustramos con un ejemplo la interoperabilidad de las herramientas disponibles en su versión actual.