Declarative Debugging of Missing Answers for Maude

13 years 6 months ago
Declarative Debugging of Missing Answers for Maude
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 error. Membership equational logic (MEL) is an equational logic that in addition to equations allows to state of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative d...
Adrián Riesco, Alberto Verdejo, Narciso Mar
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where RTA
Authors Adrián Riesco, Alberto Verdejo, Narciso Martí-Oliet
Comments (0)