Occurences in Debugger Specifications

Abstract

We describe formal manipulations of programming language semantics that permit execution animation for interpreters. We first study the use of occurrences in the -calculus and we describe an implementation of the notion of residuals. We then describe applications in the development of interpreters for the lazy -calculus and the parallel language Occam. 1. Introduction Formal descriptions of programming language semantics have already been shown to yield executable specifications of interpreters for these languages [Mini-ML], [Esterel]. However, while the obtained interpreters have the clear advantage of being "certified" implementations, they lack a nice user interface for the very reason that the definition only deals with semantic values. An interpreter can be tranformed into a debugging tool by adding tracing, profiling, or control of execution functionalities. For us, an execution trace is a list of basic instruction calls that describes a history of execution, a profile is a list...