Operational Semantics of a Focusing Debugger

This paper explores two main ideas: (1) a debugger for a programming language ought to have a formal semantic definition that is closely allied to the formal definition of the language itself; and (2) a debugger for very high level programming language ought to provide support for exposing hidden information in a controlled fashion. We investigate these ideas by giving formal semantic definitions for a simple functional programming language and an associated debugger for the language. The formal definitions are accomplished using structured operational semantics, and they demonstrate one way in which the formal definition of a debugger might be built "on top of" the formal definition of the underlying language. The debugger itself provides the novel capability of allowing the programmer to "focus" or shift the scope of attention in a syntax-directed fashion to a specific subexpression within the program, and to view the execution of the program from that vantage. The main formal result about the debugger is that "focusing preserves meaning," in the sense that a program being debugged exhibits equivalent (bisimilar) operational behavior regardless of the subexpression to which the focus has been shifted.