CafeInMaude: A CafeOBJ Interpreter in Maude

摘要

We present in this paper CafeInMaude, an interpreter for non-behavioral CafeOBJ specifications. The interpreter has been implemented in Maude. This alternative implementation combines CafeOBJ specification and theorem proving capabilities with efficient and extensible Maude commands and tools. Hence, it makes it possible to use both CafeOBJ proof scores and reduction commands and Maude model checking, narrowing, or theorem proving capabilities with the same tool.