A declarative debugger for Maude functional modules

In G. Rosu, editor, Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, ENTCS 238(3), pages 63-81. Elsevier, 2009. © Elsevier

Abstract: A declarative debugger for Maude functional modules, which correspond to executable specifications in membership equational logic, is presented. Starting from an incorrect computation, declarative debugging builds a debugging tree as a logical representation of the computation, that then is traversed by asking questions to an external oracle until the error is found. We summarize the construction of appropriate debugging trees for oriented equational and membership inferences, where all the nodes whose correctness does not need any justification have been collapsed. The reflective features of Maude allow us to generate and navigate the debugging tree of a Maude computation using operations in Maude itself; even the user interface of the declarative debugger can be specified in this way. We present the debugger's 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, selection of trusted vs. suspicious statements by means of labels, and trusting of statements "on the fly".

[pdf]

@inproceedings{CMORV08-wrla,
	Author = {Rafael Caballero and Narciso Mart\'{\i}-Oliet and Adri\'an Riesco and Alberto Verdejo},
	Booktitle = {Proceedings of the Seventh International Workshop on 
	             Rewriting Logic and its Applications, WRLA 2008},
	Editor = {Grigore Ro\c{s}u},
	Number = {3},
	Pages = {63-81},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {A declarative debugger for {Maude} functional modules},
	Volume = {238},
	Year = {2009}}