Abstract Diagnosis of Functional Programs

Abstract Diagnosis of Functional Programs

by María Alpuente, Marco Comini, Santiago Escobar, Moreno Falaschi, and Salvador Lucas.

Description

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 T_P, 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 [ACEFL03], we develop a preliminary 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 have refined our methodology in [ACEF06].

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 T_R 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 T_R 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 T^k_R and, by a simple static test, we can determine all the rules which are wrong w.r.t. the considered abstract property.

Download

A prototype Haskell interpreter has been developed in Hugs and is available here. The prototype tool is able to read TRSs in a naive and simple syntax as well as programs in OBJ syntax. The system includes options to manipulate a program or combine several ones. Incorrect and uncovered rules of the TRS w.r.t. the intended semantics are detected and shown by the tool. The abstraction of the intended semantics is also shown during the execution.

References

[ACEFL03] M. Alpuente, M. Comini, S. Escobar, M. Falaschi, and S. Lucas. Abstract Diagnosis of Functional Programs. In M. Leuschel, editor, Springer LNCS 2664:1-16, 2003.

[ACEF06] M. Alpuente, M. Comini, S. Escobar, M. Falaschi. A Compact Semantics FixPoint Semantics for Term Rewriting Systems, 2006.

[BN98] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[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.

[CLMV96b] M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Abstract Diagnosis. Journal of Logic Programming, 39(1-3):43-93, 1999.

[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.

[Cousot02] P. Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Theoretical Computer Science, 1-2:47-103, 2002.

[Ferrand87] G. Ferrand. Error Diagnosis in Logic Programming, an Adaptation of E. Y. Shapiro's Method. Journal of Logic Programming, 4(3):177-198, 1987.

[Klop92] J. W. Klop. Term Rewriting Systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume I, pages 1-112. Oxford University Press, 1992.

[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.

[NF94] H. Nilsson and P. Fritzson. Algoritmic debugging for lazy functional languages. Journal of Functional Programming, 4(1):337-370, 1994.

[OH88] J. T. O'Donell and C. V. Hall. Debugging in Applicative Languages. Lisp and Symbolic Computation, 1(2):113-145, 1988.

[PE93] R. Plasmeijer and M. van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading, MA, 1993.

[Shapiro82] E. Y. Shapiro. Algorithmic Program Debugging. In Proceedings of Ninth Annual ACM Symp. on Principles of Programming Languages, pages 412-531. ACM Press, 1982.

[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.

[Toyn98] I. Toyn. Exploratory Environments for Functional Programming. PhD thesis, University of York, U.K., 1987.

[Wadler98] P. Wadler. Functional Programming: An angry half-dozen. Volume 33 of SIGPLAN Notices, pages 25-30. ACM Press, 1998.

Last update Dec 2002 # sescobar@dsic.upv.es