Given the different perspectives from which a complex software
system has to be analyzed, the multiplicity of formalisms is in some sense
unavoidable. This poses two important technical challenges: how to rigorously
meet the need to inter-relate formalisms, and how to reduce the duplication of
effort in tool and specification building across formalisms. These challenges
could be answered by adequate *formal meta-tools* that, when given the
specification of a formal inference system, generate an efficient inference
engine, and when given a specification of two formalism and a translation,
generate an actual translator between them. Similarly, module composition
operations that are logic-independent, but that at present require costly
implementation efforts for each formalism could be provided for logics in
general by module algebra generator meta-tools. The foundations of meta-tools
of this kind can be based on a meta-theory of general logics. Their actual
design and implementation can be based on appropriate logical frameworks
having efficient implementations. This paper explains how the reflective
logical framework of rewriting logic can be used, in conjunction with an
efficient reflective implementation such as the Maude language, to design
formal meta-tools such as those described above. The feasibility of these
ideas and techniques has been demonstrated by a number of substantial
experiments in which new formal tools and new translations between formalisms,
efficient enough to be used in practice, have been generated.

(BibTeX entry) (gzip'ed Postscript)

back home Formal Methods and Declarative Languages Laboratory Computer Science Laboratory, SRI International