A Debugging System Based on Natural Semantics1

Due to the absence of side effects, reasoning about functional programs is simpler than reasoning about their imperative counterparts. However, because of the absence of practical debuggers, finding bugs in lazy functional languages has been more complex until quite recently. One of the easiest to use Haskell debuggers is Hood. Its behavior is based on the concept of observation of intermediate data structures. However, although using Hood can be simple when observing some structures, it is known that it can be hard to understand how it works when dealing with complex situations. In fact, the author of Hood recognizes that it is necessary to formalize its behavior to explain better what should be expected, and also to allow to check whether the different implementations work properly. In this paper, we formalize the behavior of the Hood debugger by extending Sestoft’s natural semantics. Moreover, we also show how to derive an abstract machine including such debugging information. By doing so, we do not only provide a formal foundation, but we also provide an alternative method to implement debuggers. In fact, we have already made a prototype of the abstract machine presented in this paper.