BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/focus.ps.Z
       ENTRY:: November 19, 1994
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Operational Semantics of a Focusing Debugger (Full version)
        TYPE:: Preprint
      AUTHOR:: Bernstein, Karen L., and Stark, Eugene W.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 516-632-8444 <stark@cs.sunysb.edu>
	DATE:: November, 1994
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/focus.ps.gz

ABSTRACT::

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.