by María Alpuente, Marco Comini, Santiago Escobar, Moreno Falaschi, and Salvador Lucas.
Finding program bugs is a long-standing problem in software construction. This work is motivated by the fact that the debugging support for functional languages in current systems is poor [Wadler98], and there are no general purpose, good semantics-based debugging tools available.
Traditional debugging tools for functional programming languages consist of tracers which help to display the execution [OH88,Toyn87] but which do not enforce program correctness adequately as they do not provide means for finding bugs in the source code w.r.t. the intended program semantics. Declarative debugging of functional programs [NF94,Nilsson99,SN95] is a semi-automatic debugging technique where the debugger tries to locate the node in an execution tree which is ultimately responsible for a visible bug symptom. This is done by asking the user, which assumes the role of the oracle. When debugging real code, the questions are often textually large and may be difficult to answer. Abstract diagnosis [CMLV96a,CMLV96b, CLV95] is a declarative debugging framework which extends the methodology in [Ferrand87,Shapiro82], based on using the immediate consequence operator TP, to identify bugs in logic programs, to diagnosis w.r.t. computed answers. The framework is goal independent and does not require the determination of symptoms in advance.
In this work, we develop an abstract diagnosis method for functional programming which applies the ideas of [CLMV96b] to debug a functional program w.r.t. the semantics of normal forms and (ground) constructor normal forms (or values). We use the formalism of term rewriting systems as it provides an adequate computational model for functional programming languages where functions are defined by means of patterns (e.g., Haskell, Hope or Miranda) [BN98,Klop92,PE93]. We associate a (continuous) immediate consequence operator TR to program R which allows us to derive an input-output semantics for R, as in the fixpoint finite/angelic relational semantics of [Cousot02]. Then, we formulate an efficient debugging methodology, based on abstract interpretation, which proceeds by approximating the TR operator by means of a depth(k) cut [CLMV96b]. We show that, given the intended specification I of the semantics of a program R, we can check the correctness of R by a single step of the abstract immediate consequence operator TkR and, by a simple static test, we can determine all the rules which are wrong w.r.t. the considered abstract property.
[CLMV96a] M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Proving properties of Logic Programs by Abstract Diagnosis. In M. Dams, editor, Proceedings of Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop (LOMAPS'96), LNCS 1192, pages 22-50, Berlin, 1996. Springer-Verlag.
[CLV95] M. Comini, G. Levi, and G. Vitiello. Declarative Diagnosis Revisited. In J. W. Lloyd, editor, Proceedings of the 1995 Int'l Symposium on Logic Programming (ILPS'95), pages 275-287, Cambridge, Mass., 1995. The MIT Press.
[Nilsson99] H. Nilsson. Tracing piece by piece: affordable debugging for lazy functional languages. In Proceedings of the 1999 ACM SIGPLAN Int'l Conf. on Functional Programming}, pages 36-47. ACM Press, 1999.
[SN95] J. Sparud and H. Nilsson. The architecture of a debugger for lazy functional languages. In M. Ducassé, editor, Proceedings of the Second International Workshop on Automated and Algorithmic Debugging, AADEBUG'95, 1995.
[Wadler98] P. Wadler. Functional Programming: An angry half-dozen. Volume 33 of SIGPLAN Notices, pages 25-30. ACM Press, 1998.
Last update Dec 2002 # email@example.com