## 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