Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications (Extended Version)
Min Zhang, Kazuhiro Ogata · Institutional Repositories DataBase (IRDB) · 2010
Specification translation plays an important part in the integration of theorem proving and model checking techniques for system verification. Mucheffort is required to implement a translation tool in conventional programming languages. Maude provides powerful meta-programming facilities that allow us to develop formal translation tools with less effort. In this paper, we present a modular implementation of a translator that is developed in Maude. The translator takes a behavioral specification and produces a rewrite theoryspecification. The implementation of the translator is modular so that multiple translation strategies can be modularized and embedded in the translator.Therefore, multiple styles of rewrite theory specifications can be generated for one behavioral specification.