Introducing CafeOBJ specifications in the Full Maude database. Integrating CafeOBJ with the Constructor-based Inductive Theorem Prover—Programmer Guide

CafeOBJ and Maude are sister languages of the OBJ language, and two of the most advanced formal specification languages for systems verification. Although both of them have a similar syntax and semantics, different usages and applications have been developed for them. Hence, a tool combining both languages would be very useful for exploiting the specific features of each of them. We present here the details of the implementation to load CafeOBJ specifications into the Full Maude. We first show how to define the syntax, the functions for parsing, and the rules to deal with general commands. Then, we present how to extend a specific tool, the Constructor-based Inductive Theorem Prover (CITP), to deal with CafeOBJ specifications. This is achieved by creating an attribute that distinguishes the current language, combining the syntax of both tools, and defining rules that deal with the commands when our ne