A Declarative Debugger for Maude Specifications: User Guide

Abstract

We show in this guide how to use our declarative debugger for Maude specifications. Declarative debugging is a semi-automatic technique that starts from a computation considered incorrect by the user (error symptom) and locates a program fragment responsible for the error by asking questions to an external oracle, which is usually the user. In our case the debugging tree is obtained from a proof tree in a suitable semantic calculus; more concretely, we abbreviate the proof trees obtained from this calculus in order to ease and shorten the debugging process while preserving the correctness and completeness of the technique. We present the main features of our tool, what is assumed about the modules introduced by the user, the list of available commands, and the kinds of questions used during the debugging process. Then, we use several examples to illustrate how to use the debugger. We refer the interested reader to the webpage http://maude.sip.ucm.es/debugging, where these and other examples can be found together with more information about the theory underlying the debugger, its implementation and the Maude source files.