Towards an algebraic specification of code generation (Q1121033)

The authors show how the problem of code generation can be treated fully algebraically. They demonstrate the approach by specifying the compiler for a very simple language, which describes arithmetic expressions. The authors first define the abstract syntax and the semantics of this language and then that of the target language. For this purpose, they use a stack machine. The main section of the paper defines the code generator as an operation of an appropriate abstract data type and proves this translation to be correct. The proof clarifies the major advantage of this approach: Theorems about the code generator can be proved by induction on the term structure of the abstract syntax. In addition, the authors consider an ``a posteriori'' optimization and show that the approach is applicable to this phase, too. Finally, they mention a prototype implementation using the Passau RAP system. The paper is written very clearly and is an important step towards a uniform specification of all compiler phases.