Declarative Debugging of Membership Equational Logic Specifications

  • Rafael Caballero
  • Narciso Martí-Oliet
  • Adrián Riesco
  • Alberto Verdejo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


Algorithmic debugging has been applied to many declarative programming paradigms; in this paper, it is applied to the rewriting paradigm embodied in Maude. We introduce a declarative debugger for executable specifications in membership equational logic which correspond to Maude functional modules. Declarative debugging is based on the construction and navigation of a debugging tree which logically represents the computation steps. We describe the construction of appropriate debugging trees for oriented equational and membership inferences. These trees are obtained as the result of collapsing in proof trees all those nodes whose correctness does not need any justification. We use an extended example to illustrate the use of the declarative debugger and its main features, such as two different strategies to traverse the debugging tree, use of a correct module to reduce the number of questions asked to the user, and selection of trusted vs. suspicious statements by means of labels. The reflective features of Maude have been extensively used to develop a prototype implementation of the declarative debugger for Maude functional modules using Maude itself.


declarative debugging membership equational logic Maude functional modules 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alpuente, M., Comini, M., Escobar, S., Falaschi, M., Lucas, S.: Abstract diagnosis of functional programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 1–16. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Caballero, R.: A declarative debugger of incorrect answers for constraint functional-logic programs. In: WCFLP 2005: Proceedings of the 2005 ACM SIGPLAN Workshop on Curry and Functional Logic Programming, pp. 8–13. ACM Press, New York (2005)CrossRefGoogle Scholar
  4. 4.
    Caballero, R., Martí-Oliet, N., Riesco, A., Verdejo, A.: Declarative debugging of Maude functional modules. Technical Report 4/07, Dpto.Sistemas Informáticos y Computación, Universidad Complutense de Madrid (2007),
  5. 5.
    Caballero, R., Rodríguez-Artalejo, M.: DDT: A declarative debugging tool for functional-logic languages. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 70–84. Springer, Heidelberg (2004)Google Scholar
  6. 6.
    Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, Stanford University (2000)Google Scholar
  7. 7.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  8. 8.
    Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theoretical Computer Science 285(2), 245–288 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Comini, M., Levi, G., Meo, M.C., Vitiello, G.: Abstract diagnosis. Journal of Logic Programming 39(1-3), 43–93 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Lloyd, J.W.: Declarative error diagnosis. New Generation Computing 5(2), 133–154 (1987)zbMATHGoogle Scholar
  11. 11.
    MacLarty, I.: Practical Declarative Debugging of Mercury Programs. PhD thesis, University of Melbourne (2005)Google Scholar
  12. 12.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)Google Scholar
  14. 14.
    Naish, L.: Declarative diagnosis of missing answers. New Generation Computing 10(3), 255–286 (1992)Google Scholar
  15. 15.
    Naish, L.: A declarative debugging scheme. Journal of Functional and Logic Programming 1997(3), 1–27 (1997)Google Scholar
  16. 16.
    Nilsson, H.: How to look busy while being as lazy as ever: the implementation of a lazy functional debugger. Journal of Functional Programming 11(6), 629–671 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Nilsson, H., Fritzson, P.: Algorithmic debugging of lazy functional languages. Journal of Functional Programming 4(3), 337–370 (1994)CrossRefGoogle Scholar
  18. 18.
    Pope, B.: Declarative debugging with Buddha. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 273–308. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Shapiro, E.Y.: Algorithmic Program Debugging. ACM Distinguished Dissertation. MIT Press, Cambridge (1983)Google Scholar
  20. 20.
    Silva, J.: A comparative study of algorithmic debugging strategies. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 143–159. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  21. 21.
    Takahashi, N., Ono, S.: DDS: A declarative debugging system for functional programs. Systems and Computers in Japan 21(11), 21–32 (1990)CrossRefGoogle Scholar
  22. 22.
    Tessier, A., Ferrand, G.: Declarative diagnosis in the CLP scheme. In: Analysis and Visualization Tools for Constraint Programming, Constraint Debugging (DiSCiPl project), pp. 151–174. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  23. 23.
    Wadler, P.: Why no one uses functional languages. SIGPLAN Not. 33(8), 23–27 (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Rafael Caballero
    • 1
  • Narciso Martí-Oliet
    • 1
  • Adrián Riesco
    • 1
  • Alberto Verdejo
    • 1
  1. 1.Facultad de InformáticaUniversidad Complutense de MadridSpain

Personalised recommendations