R.: A declarative debugger for Maude

Abstract. Declarative debugging has been applied to many declarative program-ming paradigms; in this paper, a declarative debugger for rewriting logic specifi-cations, embodied in the Maude language, is presented. Starting from an incorrect computation (a reduction, a type inference, or a rewrite), the debugger builds a tree representing this computation and guides the user through it to find a wrong statement. We present the debugger’s main features, such as support for func-tional and system modules, two possible constructions of the debugging tree, two different strategies to traverse it, use of a correct module to reduce the number of questions asked to the user, selection of trusted vs. suspicious statements, and trusting of statements “on the fly”.