[Maude-users] 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://maude.cs.uiuc.edu/pipermail/maude-users/attachments/20080118/5e146b2e/attachment.htm