Improving the Debugging of Membership Equational Logic Specifications∗

PROMESAS (S0505/TIC/0407), TIN2008-06622-C03-01, S-0505/TIC/0407, and UCM-BSCH-GR58/08-910502. 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 take