zbMATH — the first resource for mathematics

Operational semantics of a focusing debugger. (English) Zbl 0910.68128
Brookes, Steve (ed.) et al., Mathematical foundations of programming semantics. Proceedings of the 11th conference (MFPS), Tulane Univ., New Orleans, LA, USA, March 29 - April 1, 1995. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 1, 19 p. (1995).
Summary: 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 ab out 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.
For the entire collection see [Zbl 0903.00064].

68Q55 Semantics in the theory of computing
Full Text: Link