Improving the debugging of membership equational logic specifications

Technical report SIC-2/11, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, April 2011.

Abstract: Declarative debugging is a debugging technique that abstracts the execution details, that can be difficult to follow in general in declarative languages, to focus on results. It relies on a data structure called debugging tree, that represents the computation and is traversed by asking questions to the user about the correction of the computation steps related to each node. Thus, the complexity of the questions is an important factor regarding the applicability of the technique. In this paper we present a transformation for debugging trees for Maude specifications that ensures that any subterm occurring in a question has been previously replaced by the most reduced form that it has taken during the computation, thus ensuring that questions become as simple as possible..

[pdf]

@techreport{debstratTR11,
	Author = {Rafael Caballero and Adri\'an Riesco and Alberto Verdejo and Narciso Mart\'{\i}-Oliet},
	Institution = {Dpto.\ Sistemas Inform\'aticos y Computaci\'on, Universidad Complutense de Madrid},
	Number = {SIC-02/11},
	Title = {Improving the debugging of membership equational logic specifications},
	Ee = {http://maude.sip.ucm.es/debugging},
	Year = {2011}}