Observational Equivalence and Compiler Correctness

Fabio Q B da Silva

Abstract: In this work, we study the problem of giving proofs of compiler correctness in the framework of observational equivalence and correspondences. The starting point for correctness is a formal semantics of the programming language given in a form of Structural Operational Semantics which we call Relational Semantics. Intuitively, the problem of compiler correctness consists in establishing whether a compiler for a programming language generates ``correct machine code'' for programs in the language. The key aspect of this problem is to define a natural and formal meaning for ``correct machine code''.

We start by introducing Relational Semantics. We then define an equivalence relation between Relational Semantics based on the notion of observational equivalence and extend the proof method of correspondences to a proof method for observational equivalence of Relational Semantics which we call Model Correspondence. The main theoretical result of this work shows that Model Correspondence is sound and complete with respect to observational equivalence and therefore can be used as a proof method.

Finally we use observational equivalence to establish the equivalence between a (standard) semantics of the programming language and another semantics defined using a compilation of the language into some machine code. This notion of equivalence defines a criterion for compiler correctness and we shall argue why this is a suitable criterion. We also show a proof of compiler correctness that illustrates the use of Model Correspondence.

LFCS report ECS-LFCS-92-240, September 1992.

Previous | Index | Next