• People
• Events
• Research

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

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)