Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications

Meta-level facilities of Maude allow us to develop formal tools with less effort than conventional programming languages. We present a modular implementation of a translator with meta-level facilities of Maude. The translator takes a behavioral specification and produces behaviorally equivalent rewrite theory specifications. The implementation of the translator is modular so that multiple translation strategies can be modularized and embedded in it. Multiple styles of rewrite theory specifications can be automatically generated for one behavioral specification.