Declarative debugger for Maude functional modules

[Adrián Riesco]

Dear friends,

We have developed a new type of debugger for Maude functional modules based on declarative

debugging. The debugging process starts with an incorrect transition from the initial term to a fully

reduced unexpected one. Our debugger, after building a proof tree for that inference, will present

to the user questions similar to “Is it correct that T fully reduces to T' ?”, which in general are easier

to answer. Moreover, since the questions are located in the proof tree, the answer allows the debugger

to discard a subset of the questions, leading and shortening the debugging process.

The current version of the tool has the following characteristics: 

• It supports all kinds of functional modules (except for the attribute strat). 

• It provides two strategies to traverse the debugging tree: top-down, that traverses  the tree from the root

asking each time for the correctness of all the children of the current node, and then continues with one

of the incorrect children; and divide and query, that each time selects the node whose subtree’s size is

the closest one to half the size of the whole tree, keeping only this subtree if its root is incorrect, and 

deleting the whole subtree otherwise. 

• Before starting the debugging process, the user can select a module containing only correct statements.

By checking the correctness of the inferences with respect to this module the debugger can reduce the

number of questions asked to the user.

• It allows to debug Maude functional modules where some equations and memberships are suspicious and

have been labeled (each one with a different label). Only these labeled statements generate nodes in the

proof tree. 

• When the debugger is started, it allows to select the list of labeled statements that will be used to generate

the proof tree, thus restricting the debugged statements. Moreover, the user can answer that he trusts the

statement associated with the currently questioned inference; that is, statements can be trusted “on the fly.”

The debugger source files, as well as documentation and examples, are available from

http://maude.sip.ucm.es/debugging/. Periodical updates will be published in this page.

We hope you will find it useful. Comments and suggestions are welcome.

Best regards,

 R. Caballero, N. Martí-Oliet, A. Riesco, and A. Verdejo

_______________________________________________
Maude-users mailing list
Maude-users@...
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users