Declarative Debugging of Rewriting Logic Specifications

In A. Corradini and U. Montanari, editors, Recent Trends in Algebraic Development Techniques. 19th International Workshop, WADT 2008, LNCS 5486, pages 308-325. Springer, 2009. © Springer-Verlag

Abstract: Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the wrong statement. This paper presents the fundamentals for the declarative debugging of rewriting logic specifications, realized in the Maude language, where a wrong computation can be a reduction, a type inference, or a rewrite. We define appropriate debugging trees obtained as the result of collapsing in proof trees all those nodes whose correctness does not need any justification. Since these trees are obtained from a suitable semantic calculus, the correctness and completeness of the debugging technique can be formally proved. We illustrate how to use the debugger by means of an example and succinctly describe its implementation in Maude itself thanks to its reflective and metalanguage features.

[pdf]

@inproceedings{RVMC08-wadt,
	Author = {Adri\'an Riesco and Alberto Verdejo and Rafael Caballero and Narciso Mart\'{\i}-Oliet},
	Title = {Declarative Debugging of Rewriting Logic Specifications},
	Booktitle = {Recent Trends in Algebraic Development Techniques (WADT 2008)},
	Editor = {Andrea Corradini and Ugo Montanari},
	Pages = {308-325},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Volume = {5486},
	Year = {2009}}