## Correctness Proofs of Compilers and Debuggers: an Approach
Based on Structural Operational Semantics

**Fabio Q B da Silva**
*Abstract:* In this thesis we study the use of
semantics-based formal methods in the specification and proof of
correctness of compilers and debuggers. We use a Structural
Operational Semantics as the basis for the specification of
compilers and propose a notion of correctness based on an
observational equivalence relation. We define program evaluation
and a notion of evaluation step based on a Structural Operational
Semantics and use these definitions as the basis for the
specification of debuggers. Debugger correctness is then defined by
an equivalence relation between a specification and an
implementation of the debugger based on the bisimulation
concept.

The main results of this thesis are a definition of a variant of
Structural Operational Semantics, called Relational Semantics,
which is the underlying formalism of this thesis; the definition of
a notion of Observational Equivalence between Relational Semantics
Specifications; a formulation of the problem of compiler
correctness using Observational Equivalence; an evaluation model
for programming languages and a definition of an evaluation step;
an abstract definition of Inerpreter-debuggers; a specification
notation for the formal specification of debuggers, called DSL; a
notion of equivalence between debuggers using bisimulation; a study
on Compiler-debuggers and the problems involved in their
definition.

These results form a theory for the formal specification and
proofs of correctness of compilers and debuggers. Our starting
point is that the use of this theory helps in building better
compilers and debuggers. It is our goal to provide theoretical
foundations and tools to show that our methods are achievable.

**PhD Thesis - Price £9.00**

*LFCS report ECS-LFCS-92-241 (also published as
CST-95-92)*

Previous |

Index |

Next