A zoom-declarative debugger for sequential Erlang programs

• Present a declarative approach for debugging the sequential part of Erlang.
• Provide debugging granularity: it can find erroneous functions and bugs in functions code.
• Develop a tool and test it with real Erlang programs, obtaining promising usability results.
• Introduce a formalized natural semantics for sequential Core Erlang.

We present a declarative debugger for sequential Erlang programs. The tool is started when a program produces some unexpected result, and proceeds asking questions to the user about the correctness of some subcomputations until an erroneous program function is found. Then, the user can refine the granularity by zooming in the function, checking the values bound to variables and the if/case/try-catch branches taken during the execution. We show by means of an extensive benchmark that the result is a usable, scalable tool that complements already existing debugging tools such as the Erlang tracer and Dialyzer. Since the technique is based on a formal calculus, we are able to prove the soundness and completeness of the approach.