Enhancing the debugging of Maude specifications

In P. C. Olveczky, editor, Rewriting Logic and its Applications. 8th International Workshop, WRLA 2010, LNCS 6381, pages 226-242. Springer, 2010. © Springer-Verlag

Abstract: Declarative debugging is a semi-automatic technique that locates a program fragment responsible for the error by building a tree representing the computation and guiding the user through it to find the error. Two different kinds of errors are considered for debugging: wrong answers (a wrong result obtained from an initial value) and missing answers (a term that should be reachable but cannot be obtained from an initial value), where the latter has only been considered in nondeterministic systems. However, we consider that missing answers can also appear in deterministic systems, when we obtain correct results that do not provide all the expected information, which corresponds, in the context of Maude modules, to terms whose normal form is not reached and to terms whose computed least sort is, although correct, bigger than the expected one. We present in this paper a calculus to deduce normal forms and least sorts, and a proper abbreviation of the trees obtained with it. These trees increase both the causes (missing equations and memberships) and the errors (erroneous normal forms and least sorts) detected in our debugging framework.

[pdf]

@inproceedings{wrla/RiescoVM10,
	Author = {Adri{\'a}n Riesco and Alberto Verdejo and Narciso Mart\'{\i}-Oliet},
	Pages = {226-242},
	Title = {Enhancing the Debugging of {Maude} Specifications},
	ee = {http://dx.doi.org/10.1007/978-3-642-16310-4_15},
	Booktitle = {Rewriting Logic and its Applications. 8th International Workshop, WRLA 2010, 
	             Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, 
	             Revised Selected Papers},
	Editor = {Peter Csaba {\"O}lveczky},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Volume = {6381},
	Year = {2010}}