×

Declarative debugging of functional logic programs. (English) Zbl 1268.68091

Gramlich, Bernhard (ed.) et al., WRS 2001. 1st international workshop on reduction strategies in rewriting and programming, Utrecht, The Netherlands, May 26, 2001. Post-workshop proceedings. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 57, 17-40 (2001).
Summary: We present a general framework for the declarative debugging of functional logic programs, which is valid both for eager as well as lazy programs. We associate to our programs a semantics based on a (continuous) immediate consequence operator which models computed answers. Then we show that, given the intended specification of a program \(P\), it is possible to check the correctness of \(P\) by a single step of the immediate consequence operator.
We also present a more effective methodology which is based on abstract interpretation. By approximating the intended specification of the success set we derive a finitely terminating debugging method, which can be used statically. Our framework is parametric w.r.t. to the chosen approximation of the success set. We present one specific example of approximation. We provide an implementation of our debugging system which shows experimentally on a wide set of benchmarks that we are able to find some common errors in the user programs.
For the entire collection see [Zbl 1266.68016].

MSC:

68Q42 Grammars and rewriting systems
68N17 Logic programming
68N18 Functional programming and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Curry; BABEL; Kernel-LEAF
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] M. Alpuente, F. J. Correa, M. Falaschi, and S. Marson. The Debugging System BUGGYhttp://www.dsic.upv.es/users/elp/papers.html; M. Alpuente, F. J. Correa, M. Falaschi, and S. Marson. The Debugging System BUGGYhttp://www.dsic.upv.es/users/elp/papers.html
[2] Alpuente, M.; Falaschi, M.; Manzo, F., Analyses of Unsatisfiability for Equational Logic Programming, Journal of Logic Programming, 22, 3, 221-252 (1995) · Zbl 0830.68024
[3] Alpuente, M.; Falaschi, M.; Vidal, G., A Compositional Semantic Basis for the Analysis of Equational Horn Programs, Theoretical Computer Science, 165, 1, 97-131 (1996)
[4] Antoy, S.; Echahed, R.; Hanus, M., A needed narrowing strategy, Journal of the ACM, 47, 4, 776-822 (2000) · Zbl 1327.68141
[5] P. Arenas and A. Gil. A debugging model for lazy functional languages. Technical Report DIA 94/6, Universidad Complutense de Madrid, April 1994.; P. Arenas and A. Gil. A debugging model for lazy functional languages. Technical Report DIA 94/6, Universidad Complutense de Madrid, April 1994.
[6] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[7] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proc. of First European Symp. on Programming, ESOP’86; D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proc. of First European Symp. on Programming, ESOP’86 · Zbl 0587.68003
[8] D. Bert and R. Echahed. On the Operational Semantics of the Algebraic and Logic Programming Language LPG. In Recent Trends in Data Type Specifications; D. Bert and R. Echahed. On the Operational Semantics of the Algebraic and Logic Programming Language LPG. In Recent Trends in Data Type Specifications
[9] D. Bert, R. Echahed, and B.M. Østvold. Abstract Rewriting. In Proc. of Third Int’l Workshop on Static Analysis, WSA’93; D. Bert, R. Echahed, and B.M. Østvold. Abstract Rewriting. In Proc. of Third Int’l Workshop on Static Analysis, WSA’93
[10] Bosco, P.; Giovannetti, E.; Moiso, C., Narrowing vs. SLD-resolution, Theoretical Computer Science, 59, 3-23 (1988) · Zbl 0648.68043
[11] F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M Hermenegildo, J. Maluszyński, and G. Puebla. On the role of semantic approximations in validation and diagnosis of constraint logic programs. In Proc. of the 3rd. Int’l Workshop on Automated Debugging-AADEBUG’97; F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M Hermenegildo, J. Maluszyński, and G. Puebla. On the role of semantic approximations in validation and diagnosis of constraint logic programs. In Proc. of the 3rd. Int’l Workshop on Automated Debugging-AADEBUG’97
[12] R. Caballero-Roldán, F.J. López-Fraguas, and M. Rodríquez Artalejo. Theoretical Foundations for the Declarative Debugging of Lazy Functional Logic Programs. In Fifth International Symposium on Functional and Logic Programming; R. Caballero-Roldán, F.J. López-Fraguas, and M. Rodríquez Artalejo. Theoretical Foundations for the Declarative Debugging of Lazy Functional Logic Programs. In Fifth International Symposium on Functional and Logic Programming · Zbl 0977.68510
[13] R. Caballero-Roldán, F.J. López-Fraguas, and J. Sánchez-Hernández. User’s manual for Toy. Technical Report SIP-5797, UCM, Madrid (Spain), 1997.; R. Caballero-Roldán, F.J. López-Fraguas, and J. Sánchez-Hernández. User’s manual for Toy. Technical Report SIP-5797, UCM, Madrid (Spain), 1997.
[14] M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In K. Furukawa, editor, Proc. of Eighth Int’l Conf. on Logic Programming; M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In K. Furukawa, editor, Proc. of Eighth Int’l Conf. on Logic Programming
[15] M. Comini, R. Gori, and G. Levi. Logic programs as specifications in the inductive verification of logic programs. In Proceeding of Appia-Gulp-Prode’00, Joint Conference on Declarative Programminghttp://nutella.di.unipi.it/ agpOO/AccptList.html; M. Comini, R. Gori, and G. Levi. Logic programs as specifications in the inductive verification of logic programs. In Proceeding of Appia-Gulp-Prode’00, Joint Conference on Declarative Programminghttp://nutella.di.unipi.it/ agpOO/AccptList.html · Zbl 1263.68034
[16] Comini, M.; Levi, G.; Meo, M. C.; Vitiello, G., Abstract diagnosis, Journal of Logic Programming, 39, 1-3, 43-93 (1999) · Zbl 0947.68024
[17] M. Comini, G. Levi, and G. Vitiello. Declarative Diagnosis Revisited. In John W. Lloyd, editor, Proceedings of the 1995 Int’l Symposium on Logic Programming; M. Comini, G. Levi, and G. Vitiello. Declarative Diagnosis Revisited. In John W. Lloyd, editor, Proceedings of the 1995 Int’l Symposium on Logic Programming
[18] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of Fourth ACM Symp. on Principles of Programming Languages; P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of Fourth ACM Symp. on Principles of Programming Languages
[19] Dershowitz, N.; Jouannaud, J.-P., Rewrite Systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics (1990), Elsevier: Elsevier Amsterdam), 243-320 · Zbl 0900.68283
[20] W. Drabent, S. Nadjim-Tehrani, and J. Maluszynski. The use of assertions in algorithmic debugging. In Proceedings of the 1988 Iinternational Conference on Fifth Generation Computer Systems; W. Drabent, S. Nadjim-Tehrani, and J. Maluszynski. The use of assertions in algorithmic debugging. In Proceedings of the 1988 Iinternational Conference on Fifth Generation Computer Systems
[21] R. Echahed. On completeness of narrowing strategies. In Proc. of CAAP’88; R. Echahed. On completeness of narrowing strategies. In Proc. of CAAP’88 · Zbl 0645.68044
[22] R. Echahed. Uniform narrowing strategies. In Proc. of ICALP’92; R. Echahed. Uniform narrowing strategies. In Proc. of ICALP’92
[23] Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., Declarative Modeling of the Operational Behavior of Logic Languages, Theoretical Computer Science, 69, 3, 289-318 (1989) · Zbl 0699.68113
[24] Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs, Information and Computation, 103, 1, 86-113 (1993) · Zbl 0788.68088
[25] Ferrand, G., Error Diagnosis in Logic Programming, and Adaptation of E.Y. Shapiro’s Method, Journal of Logic Programming, 4, 3, 177-198 (1987) · Zbl 0623.68005
[26] L. Fribourg. SLOG: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. of Second IEEE Int’l Symp. on Logic Programming; L. Fribourg. SLOG: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. of Second IEEE Int’l Symp. on Logic Programming
[27] Giovannetti, E.; Levi, G.; Moiso, C.; Palamidessi, C., Kernel Leaf: A Logic plus Functional Language, Journal of Computer and System Sciences, 42, 363-377 (1991) · Zbl 0717.68013
[28] M. Hanus. Compiling Logic Programs with Equality. In Proc. of 2nd Int’l Workshop on Programming Language Implementation and Logic Programming; M. Hanus. Compiling Logic Programs with Equality. In Proc. of 2nd Int’l Workshop on Programming Language Implementation and Logic Programming
[29] Hanus, M., The Integration of Functions into Logic Programming: From Theory to Practice, Journal of Logic Programming, 19&20, 583-628 (1994) · Zbl 0942.68526
[30] M. Hanus and B. Josephs. A debugging model for functional logic programs. In M. Bruynooghe and J. Penjam, editors, Proc. of 5th Int’l Symp. on Programming Language Implementation and Logic Programmingvolume 714Lecture Notes in Computer Science; M. Hanus and B. Josephs. A debugging model for functional logic programs. In M. Bruynooghe and J. Penjam, editors, Proc. of 5th Int’l Symp. on Programming Language Implementation and Logic Programmingvolume 714Lecture Notes in Computer Science · Zbl 0791.68019
[31] M. Hanus, H. Kuchen, and J.J. Moreno-Navarro. Curry: A Truly Functional Logic Language. In Proc. ILPS’95 Workshop on Visions for the Future of Logic Programming; M. Hanus, H. Kuchen, and J.J. Moreno-Navarro. Curry: A Truly Functional Logic Language. In Proc. ILPS’95 Workshop on Visions for the Future of Logic Programming
[32] M. Hanus and C. Prehofer. Higher-Order Narrowing with Definitional Trees. In Proc. Seventh Int’l Conf. on Rewriting Techniques and Applications, RTA’96; M. Hanus and C. Prehofer. Higher-Order Narrowing with Definitional Trees. In Proc. Seventh Int’l Conf. on Rewriting Techniques and Applications, RTA’96 · Zbl 0926.68028
[33] Hölldobler, S., Foundations of Equational Logic Programming (1989), Springer LNAI 353 · Zbl 0688.68004
[34] Klop, J. W., Term Rewriting Systems, (Abramsky, S.; Gabbay, D.; Maibaum, T., Handbook of Logic in Computer Science, volume I (1992), Oxford University Press), 1-112
[35] Lloyd, J. W., Programming in an integrated functional and logic language, Journal of Functional and Logic Programming, 3 (1999) · Zbl 0924.68056
[36] J.W. Lloyd. Declarative Programming in Escher. Technical Report CSTR-95013, Computer Science Department, University of Bristol, 1995.; J.W. Lloyd. Declarative Programming in Escher. Technical Report CSTR-95013, Computer Science Department, University of Bristol, 1995.
[37] M.J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. of Third IEEE Symp. on Logic In Computer Science; M.J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. of Third IEEE Symp. on Logic In Computer Science
[38] M.J. Maher. On Parameterized Substitutions. Technical Report RC 16042, IBM - T.J. Watson Research Center, Yorktown Heights, NY, 1990.; M.J. Maher. On Parameterized Substitutions. Technical Report RC 16042, IBM - T.J. Watson Research Center, Yorktown Heights, NY, 1990.
[39] Moreno-Navarro, J. J.; Rodríguez-Artalejo, M., Logic Programming with Functions and Predicates: The language Babel, Journal of Logic Programming, 12, 3, 191-224 (1992) · Zbl 0754.68031
[40] Naish, L.; Barbour, T., Towards a portable lazy functional declarative debugger, Australian Computer Science Communications, 18, 1, 401-408 (1996)
[41] Naish, Lee, A declarative debugging scheme, Journal of Functional and Logic Programming, 1997, 3 (April 1997)
[42] U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. of Second IEEE Int’l Symp. on Logic Programming; U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. of Second IEEE Int’l Symp. on Logic Programming
[43] Shaphiro, E. Y., Algorithmic Program Debugging (1982), The MIT Press: The MIT Press Cambridge, Massachusetts, ACM Distinguished Dissertation.
[44] F. Zartmann. Denotational Abstract Interpretation of Functional Logic Programs. In P. Van Hentenryck, editor, Proc. of the 4th Int’l Static Analysis Symposium, SAS’97; F. Zartmann. Denotational Abstract Interpretation of Functional Logic Programs. In P. Van Hentenryck, editor, Proc. of the 4th Int’l Static Analysis Symposium, SAS’97
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.