|||Andreas Heberle, Welf LĂ¶we, Martin Trapp, Safe Reuse of Source to Intermediate Language Compilations, Proceedings of the ISSRE'98, Nov 1998.
This paper gives a short description of a framework, allowing the reuse of locally verified or at least validated transformations to generate globally correct compilers from source to intermediate languages. We introduce a calculus with normal forms to define the operational semantics of programs. Source and intermediate languages are defined in terms of this calculus. The reduction of a term to its normal form specifies a transformation. Each reduction step of the calculus is proved correct, i.e. preserves the semantics. New terms and reductions may be defined provided this correctness can be proved as well. The terms and transformations are structured by an object-oriented library. New terms are modeled by new classes, their reduction by a distinguished method that maps the new to already known classes. This construction follows the principle of substitutability that guarantees correctness by construction. For each construct of terms in normal form we define a transformation to constructs of the intermediate language in question. This definition follows the same construction principles. Since normal form terms are low level, this transformation is often a one-to-one relation or supported by standard transformations, e.g for memory mapping or building of basic blocks. Our intention is that the library accumulates to a tool supporting major parts of compilers for various source and intermediate languages.