Although there is a large body of literature on formal definitions of programming languages, relatively little work has been done in applying formal techniques to defining debuggers. In this paper, we explore the issues involved in formally defining debuggers by comparing three such attempts. Fabio da Silva has used natural operational semantics as a framework for proving the correctness of debuggers. Amir Kishon has used denotational semantics as a framework for automatically generating debuggers. In an earlier work, we proposed transition operational semantics as a framework for designing novel debugging tools. Here we sketch how a simple debugger might be defined in each of these frameworks and compare the characteristics of each of the semantic definitions.

AADEBUG'95 Program

AADEBUG'95 home page