Maude is a declarative language based on both equational and rewriting logic for the specification and implementation of a whole range of models and systems. Here we present a declarative debugger for Maude functional, system, and object-oriented modules. Functional modules define data types and operations on them by means of membership equational logic theories that support multiple sorts, subsort relations, equations, and assertions of membership in a sort. System modules specify rewrite theories that also support rules, defining local concurrent transitions that can take place in a system. Object-oriented modules support a more convenient syntax for this kind of systems.
The debugging process starts with an incorrect transition from an initial term. Our debugger, after building a proof tree for that inference, will present to the user questions about the computation. 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 supports all kinds of modules, debugging of both wrong and missing answers, different ways of trusting statements, two possible constructions of the debugging tree for rewritings, and two strategies for traversing it among many other features. The debugger is implemented on top of Full Maude, taking advantage of the reflective capabilities of Maude.
In order to use the command-line debugger you have to download dd.maude.
This version of the debugger works with Maude 2.5 and Maude 2.6.
A version for Maude 2.4 is available here.
If you want to use the Graphical User Interface, then download gui-dd.zip.
This version of the GUI works with Maude 2.5 and Maude 2.6.
A version for Maude 2.4 is available here.
strat attribute. Files:
lazy lists.
The debugger is initiated in Maude by loading the file dd.maude,
which starts an input/output loop that allows the user to interact with the
tool. Then, the user can enter Full Maude modules and commands, as well
as commands for the debugger.
The user can choose between using all the labeled statements in the debugging process (by default) or selecting some of them by means of the command
(set debug select on .)
Once this mode is activated, the user can select and deselect statements by using
(debug select LABELS .) (debug deselect LABELS .)where
LABELS is a list of statement labels separated by spaces.
Moreover, all the labels in statements of a flattened module can be selected or deselected with the commands
(debug include MODULES .) (debug exclude MODULES .)where
MODULES is a list of module names separated by spaces.
Similarly, the user can select to include or exclude from the debugging process
only a certain kind of statements. The following commands include and exclude the
equations, memberships and rules of the list of modules MODULES:
(debug include eqs MODULES .) (debug exclude eqs MODULES .) (debug include mbs MODULES .) (debug exclude mbs MODULES .) (debug include rls MODULES .) (debug exclude rls MODULES .)
The selection mode can be switched off by using the command
(set debug select off .)
In a similar way, it is also possible to indicate that some terms are final, that is, that they cannot be further rewritten:
final in the attribute metadata
of an operator, that indicates that the terms built with this operator
at the top are final.ctor) are considered final.In the first two cases, the user must activate the final sorts mode with the command
(set final select on .)
While the attribute metadata must be written in the
Maude file, final sorts can be selected/deselected with the commands
(final select SORTS .) (final deselect SORTS .)where
SORTS is a list of sort identifiers separated by
spaces.
This option can be switched off with the command
(set final select off .)
A module with only correct definitions can be used to reduce the number of questions. In this case, it must be indicated before starting the debugging process with the command
(correct with MODULE-NAME .)and can be deselected with the command
(delete correct module .)
Since rewriting is not assumed to terminate, a bound, which is 42 by default, is used when searching in the correct module and can be set with the command
(set bound BOUND .)where
BOUND is either a natural number or the constant
unbounded. Note that if it is 0 the correct module will
not be used, while if it is unbounded the correct module
is assumed to be terminating.
When debugging wrong rewrites, two different trees can be built: one whose questions are related to one-step rewrites and another whose questions are related to several steps. The user can switch between these trees, before starting the debugging process, with the commands
(one-step tree .) (many-steps tree .)being the first the default one.
In the same way, when debugging missing answers we distinguish between trees whose nodes are related to sets of terms obtained with one (the default case) or many steps. The user can select them with the commands
(one-step missing tree .) (many-steps missing tree .)
The generated debugging tree can be navigated by using two different strategies, namely, top-down and divide and query, being the latter the default one. The user can switch between them in any moment by using the commands
(top-down strategy .) (divide-query strategy .)
When debugging missing answers, the user can prioritize questions related to the fulfillment of the search condition from questions involving the statements defining it. This option, switched off by default, can be activated with the command
(solutions prioritized on .)and can be switched off again with
(solutions prioritized off .)
The debugging process for wrong answers is started with the commands
(debug [in MODULE-NAME :] INITIAL-TERM -> WRONG-TERM .) (debug [in MODULE-NAME :] INITIAL-TERM : WRONG-SORT .) (debug [in MODULE-NAME :] INITIAL-TERM =>* WRONG-TERM .)for wrong reductions, memberships, and rewrites, respectively.
MODULE-NAME is the module where the inference took place;
if no module name is
given, the current module is used by default.
Similarly, we start the debugging of missing
answers with the commands
(missing [in MODULE-NAME :] INITIAL-TERM -> FINAL-TERM .) (missing [in MODULE-NAME :] INITIAL-TERM : LEAST-SORT .)for missing answers in functional modules and
(missing [[depth]] [in MODULE-NAME :] INITIAL-TERM =>* PATTERN [s.t. CONDITION] .) (missing [[depth]] [in MODULE-NAME :] INITIAL-TERM =>+ PATTERN [s.t. CONDITION] .) (missing [[depth]] [in MODULE-NAME :] INITIAL-TERM =>! PATTERN [s.t. CONDITION] .)for missing answers in system modules, where the first command specifies a search in zero or more steps, the second one in one or more steps, and the last one only returns final terms. The
depth argument indicates the bound in the number of steps allowed
in the search, and it is considered unbounded when omitted,
while MODULE-NAME has the same behavior as in the commands above.
How the process continues depends on the selected strategy. In the divide and query strategy, each question refers to one inference that can be either correct or wrong. The different answers are transmitted to the debugger with the answers
(yes .) (no .)
If the question asked is too difficult, the user can avoid to answer it with
(don't know .)
In addition to these general answers, others can be introduced
depending on the kind of question. If it corresponds to
the application of a statement,
instead of just answering yes,
we can also trust some statements on the fly if
we decide the bug is not there. To trust the current
statement we answer
(trust .)
If a question refers to a set of reachable terms and one of these terms is not reachable, the user can point it out with the answer
(I is wrong .)where
I is the index of the wrong term in the set.
With this answer the debugger focuses then on debugging this wrong inference.
In case the question is related to a set of reachable solutions, if one of the solutions is reachable but it should not fulfill the search condition, the user can indicate it with
(I is not a solution .)where
I is the index of the term that should not be in
the set. With this answer the user indicates that the definition of the
search condition is erroneous and the debugger centers on it to continue
the process.
If the question is about a final term, additional information can be given by answering
(its sort is final .)that indicates to the debugger that all the constructed terms with the same sort as this term are final.
In case the top-down strategy is selected, several questions
will be displayed in each step. The user can introduce then
answers of the form (N : answer .), where N
is the index of the question and answer is
the same answer that would be used in the divide and query strategy
for this question.
Thus, if there is an invalid question,
the user can point it out with the answer
(N : no .)while correct questions are answered with
(N : yes .)
As a shortcut to answer (yes .) to all the questions,
the debugger provides the answer
(all : yes .)
When the user considers that a question is too complicated, it can be discarded with
(N : don't know .)
If one of the questions is associated to a program statement and the user decides that it can be trusted, it is indicated with
(N : trust .)
When a question presents an inference from a
term to a set of terms, and the term in position I is not
reachable from the initial one, then we can point it out with
(N : I is wrong .)focusing then the debugging process on this wrong computation.
Furthermore, if the question refers to the set of reachable solutions, we can identify a reachable term that does not fulfill the search condition with the command
(N : I is not a solution .)where
I the index of the term in the set. With this
answer the debugger concentrates on the definition of the search condition.
If one of the questions is related with a final term, on the fly information is given with
(N : its sort is final .)
Finally, we can return to the previous state in both strategies by using the command
(undo .)
We illustrate how to use the debugger by means of examples. A debugging session is started by
loading into Maude the file dd.maude (which already includes the Full Maude implementation).
Then, Full Maude modules and commands can be
entered, as well as commands for the debugger.