Tool Interoperability in the Maude Formal Environment
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....
- Autores:
-
Durán, Francisco
Rocha, Camilo
Álvarez, José María
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2011
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1897
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1897
- Palabra clave:
- Maude
Par crítico
Obligación de prueba
Parte Funcional
Herramienta activa
Objetivo de terminación
Critical Pair
Proof Obligation
Functional Part
Active Tool
Termination Goal
- Rights
- closedAccess
- License
- © Springer-Verlag Berlin Heidelberg 2011
| Summary: | 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. |
|---|