Abstract

Foundations for the Debugging of Functional Programs

Several debugging methods take advantage of the specific properties of functional programs, for example algorithmic debugging, following redex trails and observing expressions (a la Hood). The Haskell tracer Hat combines these methods. It records a single detailed but compact trace for the computation of a program and each method is realised in a tool that reads the trace. In this talk I will describe the structure of this trace. The trace structure is independent of any evaluation strategy. Although the trace is a graph, it is inductively defined, thus enabling inductive proofs. I will show how we can easily and efficiently perform algorithmic debugging with this trace and prove its soundness. Finally I will modify standard algorithmic debugging by representing functional values as finite maps and show how this modifies our definition of algorithmic debugging and the soundness proof.