An algebraic approach to the design of compilers for object-oriented languages

Here we describe an algebraic approach to constructing a provably correct compiler for an object-oriented language called ROOL. We tackle the problem of compiler correctness by reducing the task of compilation to that of program refinement. Compilation is identified with the reduction of a source program, written in an executable subset of the language, to a normal form. The normal form defines the behaviour of a virtual machine that executes bytecodes to implement the source program. The normal form is generated by a series of correctness-preserving transformations, which are proved correct from the basic laws of the language; These laws are proved sound with respect to a weakest precondition semantics; therefore the compilation is correct by construction.

• Type: Journal
• Year: 2010
• Where: FAC
• Authors: Adolfo Duran, Ana Cavalcanti, Augusto Sampaio
• Keywords: FAC 2010, Normal Form, Provably Correct, Source Program