Enhancing the debugging of Maude specifications

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 nonde-terministic 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 con-text 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 member-ships) and the errors (erroneous normal forms and least sorts) detected in our debugging framework