A declarative debugger for Maude specifications - User guide

Technical report SIC-7/09, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, October 2009.

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, 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.

[pdf]

@techreport{userguideTR08,
    Author = {Adri\'an Riesco and Alberto Verdejo and Rafael Caballero and Narciso Mart\'{\i}-Oliet},
    Institution = {Dpto.\ Sistemas Inform\'aticos y Computaci\'on, Universidad Complutense de Madrid},
    Number = {SIC-7/09},
    Title = {A declarative debugger for {Maude} specifications -- User guide},
    Year = {2009}}