Declarative debugging of membership equational logic specifications

In P. Degano, R. D. Nicola and J. Meseguer, editors, Concurrency, Graphs and Models, LNCS 5065, pages 174-193. Springer, 2008. © Springer

Abstract: 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.

[pdf]

@inproceedings{CMORV08-ugo,
	Author = {Rafael Caballero and Narciso Mart\'{\i}-Oliet and Adri\'an Riesco and Alberto Verdejo},
	Booktitle = {Concurrency, Graphs and Models},
	Editor = {Pierpaolo Degano and Rocco De Nicola and Jos{\'\e} Meseguer},
	Pages = {174-193},
	Publisher = {Springer},
	Series = {Lecture Notes for Computer Science},
	Title = {Declarative debugging of membership equational logic specifications},
	Volume = {5065},
	Year = {2008}}