Abstract

Foundations for Tracing Functional Programs and the Correctness of Algorithmic Debugging

The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace is a graph whose structurewas inspired by standard graph rewriting implementations of functional languages. Various ways of viewing the trace support the programmer in debugging programs and generally in comprehending programs. In the talk we describe a model ofthe Hat trace that captures its essential properties and allows formal reasoning. Definitions and proofs for the trace are more difficult than for terms, because graphs are not inductively defined and we do not want to distinguish isomorphic graphs. We will relate the trace graph to several standard views. In particular, we will show that algorithmic debugging, a semi-automatic method for locating a program fault, is correct. Our overall aim is to inspire confidence in or uncover shortcomings of existing tracing tools and improve on them.