[m-rev.] for review: document the decl debugger

[Mark Brown]

Hi,

There is still an XXX in this diff where I haven't documented
the term dependencies feature.  I'm working on that now.
The reason I'm posting this part for review now is so that
Zoltan will be able to commit his recent change that refers
to this new section.

It probably wouldn't hurt if there were multiple reviewers for this
change.

Cheers,
Mark.

Estimated hours taken: 3
Branches: main

doc/user_guide.texi:
	Document the declarative debugger.  Now that the oracle can handle
	higher order terms gracefully (if not completely), it should be
	mature enough for non-developers to try out.

Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.322
diff -u -r1.322 user_guide.texi
--- doc/user_guide.texi	22 Aug 2002 07:36:51 -0000	1.322
+++ doc/user_guide.texi	22 Aug 2002 17:52:58 -0000
@@ -75,6 +75,7 @@
 @author Zoltan Somogyi
 @author Peter Ross
 @author Tyson Dowd
+ at author Mark Brown
 @page
 @vskip 0pt plus 1filll
 Copyright @copyright{} 1995--2002 The University of Melbourne.
@@ -1158,6 +1159,7 @@
 * Mercury debugger invocation::
 * Mercury debugger concepts::
 * Debugger commands::
+* Declarative debugging::
 @end menu
 
 @node Quick overview
@@ -1595,7 +1597,8 @@
 to prepare a program for debugging,
 one that does not require the use of a debugging grade.
 With this way, you can decide, individually for each module,
-which of three trace levels, @samp{none}, @samp{shallow} and @samp{deep},
+which of five trace levels,
+ at samp{none}, @samp{shallow}, @samp{deep}, @samp{decl} and @samp{rep}
 you want to compile them with:
 
 @cindex debugger trace level
@@ -1609,10 +1612,28 @@
 @item deep
 A procedure compiled with trace level @samp{deep}
 will always generate all the events requested by the user.
-By default, this is all possible events,
+By default, this is all the usual events,
 but you can tell the compiler that
 you are not interested in some kinds of events
 via compiler options (see below).
+ at item decl
+A procedure compiled with trace level @samp{decl}
+will always generate all possible events,
+including all the events generated at trace level @samp{deep}
+as well as other events which describe
+the entry into and exit from negations.
+These events are required for the declarative debugging feature
+to operate properly,
+so the @samp{dd} command will only be available under @samp{mdb}
+at this trace level or greater.
+For more details see @ref{Declarative debugging}.
+ at item rep
+This trace level is the same as trace level @samp{decl},
+except that a representation of the module is stored in the executable
+along with the usual debugging information.
+This enables some additional declarative debugging features,
+at the cost of increasing the executable size.
+For more details see @ref{Declarative debugging}.
 @item shallow
 A procedure compiled with trace level @samp{shallow}
 will generate interface events
@@ -1634,6 +1655,15 @@
 if you suspect there may be a bug in the module,
 or if you think that being able to examine what happens inside that module
 can help you locate a bug.
+ at item decl
+You should compile a module with trace level @samp{decl}
+if you suspect there may be a bug in the module,
+and you wish to use the declarative debugger to help locate it.
+ at item rep
+You should compile a module with trace level @samp{rep}
+if you suspect there may be a bug in the module,
+you wish to use the full features of the declarative debugger,
+and you are not concerned about the size of the executable.
 @item shallow
 You should compile a module with trace level @samp{shallow}
 if you believe the code of the module is reliable and unlikely to have bugs,
@@ -1648,7 +1678,8 @@
 @end table
 
 In general, it is a good idea for most or all modules
-that can be called from modules compiled with trace level @samp{deep}
+that can be called from modules compiled with trace level
+ at samp{deep}, @samp{decl} or @samp{rep}
 to be compiled with at least trace level @samp{shallow}.
 
 You can control what trace level a module is compiled with
@@ -1659,6 +1690,10 @@
 This always sets the trace level to @samp{shallow}.
 @item --trace deep
 This always sets the trace level to @samp{deep}.
+ at item --trace decl
+This always sets the trace level to @samp{decl}.
+ at item --trace rep
+This always sets the trace level to @samp{rep}.
 @item --trace minimum
 In debugging grades, this sets the trace level to @samp{shallow};
 in non-debugging grades, it sets the trace level to @samp{none}.
@@ -1667,7 +1702,7 @@
 in non-debugging grades, it sets the trace level to @samp{none}.
 @end table
 
-As the name implies, the fourth alternative is the default,
+As the name implies, the last alternative is the default,
 which is why by default you get
 no debugging capability in non-debugging grades
 and full debugging capability in debugging grades.
@@ -1676,7 +1711,8 @@
 
 @strong{Important note}:
 If you are not using a debugging grade, but you compile
-some modules with @samp{--trace shallow} or @samp{--trace deep},
+some modules with @samp{--trace shallow}, @samp{--trace deep},
+ at samp{--trace decl} or @samp{--trace rep},
 then you must also pass the @samp{--trace} (or @samp{-t}) option
 to c2init and to the Mercury linker.
 If you're using Mmake, then you can do this by including @samp{--trace}
@@ -3007,7 +3043,246 @@
 Any answer starting with @samp{y}, or end-of-file, is considered confirmation.
 @sp 1
 End-of-file on the debugger's input is considered a quit command.
+ at sp 1
+ at item dd
+Starts declarative debugging,
+using the current event as the initial symptom.
+For details, see @ref{Declarative debugging}.
+ at end table
+
+ at node Declarative debugging
+ at section Declarative debugging
+
+The debugger incorporates a declarative debugger
+which can be accessed from its command line.
+Starting from an event which represents incorrect program behaviour,
+the declarative debugger can find a bug which explains that behaviour
+using knowledge of the intended interpretation of the program only.
+
+Note that this is a work in progress,
+so there are some limitations in the implementation.
+The main limitations are pointed out in the following sections.
+
+ at menu
+* Declarative debugging concepts::
+* Oracle questions::
+* Declarative debugging commands::
+* Diagnoses::
+ at c * Improving the search::
+ at end menu
+
+ at node Declarative debugging concepts
+ at subsection Concepts
+
+For every CALL event there is a predicate or function symbol
+for the procedure being called,
+and bindings for the input arguments to that procedure.
+In the case of a predicate, it is possible to view the event
+as a (possibly non-ground) atom
+with the given predicate symbol and bound input arguments,
+and the output arguments (if any) being distinct variables.
+In the case of a function it is also possible,
+but with equality as the predicate symbol,
+the function symbol applied to the inputs as the first argument,
+and the return value as the second argument.
+We refer to this as the @emph{call atom} of the event.
+
+The same view can be taken of EXIT events,
+although in this case the outputs as well as the inputs will be bound.
+We refer to this as the @emph{exit atom} of the event.
+The exit atom is always an instance of
+the call atom for the corresponding CALL event.
+
+Using these concepts, it is possible to interpret the following trace events
+as assertions about the semantics of the program.
+These assertions may be true or false, depending on whether or not
+the program's semantics are consistent with what was intended.
+ at sp 1
+ at table @asis
+ at item EXIT
+The assertion is that
+the exit atom is valid in the intended interpretation.
+In other words, the outputs are correct for the given inputs.
+ at sp 1
+ at item FAIL
+Every FAIL event has a matching CALL event,
+and a (possibly empty) set of matching EXIT events
+between the call and fail.
+The assertion is that
+every instance of the call atom which is true in the intended interpretation
+is an instance of one of the exit atoms.
+In other words, the complete set of answers has been given for that call.
+(Note that this does not imply that all exit atoms are correct answers;
+some exit atoms may in fact be wrong,
+but the truth of the assertion is not affected by this.)
+ at sp 1
+ at item EXCP
+Every EXCP event is associated with an exception term,
+and has a matching CALL event.
+The assertion is that the call atom can abnormally terminate
+with the given exception.
+In other words, the thrown exception was expected for that call.
+ at end table
+
+If one of these assertions is wrong,
+then we consider the event to represent incorrect behaviour of the program.
+If the user encounters an event for which the assertion is wrong,
+then they can request the declarative debugger to
+diagnose the incorrect behaviour by giving the @samp{dd} command
+to the procedural debugger at this event.
+
+ at node Oracle questions
+ at subsection Oracle questions
+
+Once the @samp{dd} command has been given,
+the declarative debugger asks the user
+a series of questions about the truth of various assertions,
+in the intended interpretation.
+The first question in this series will be about
+the event for which the @samp{dd} command was given.
+The answer to this question will nearly always be ``no'',
+since the user has just implied the assertion is false
+by giving the @samp{dd} command.
+Later questions will be about other events
+in the execution of the program,
+not all of them necessarily of the same kind as the first.
+
+The user is expected to act as an ``oracle''
+and provide answers to these questions
+based on their knowledge of the intended interpretation.
+The debugger provides some help here:
+previous answers are remembered and used where possible,
+so repeat questions are avoided.
+Commands are available to provide answers,
+as well as to browse the arguments more closely
+or to change the order in which the questions are asked.
+See the next section for details of the commands that are available.
+
+For the first type of assertion,
+a ``wrong answer'' question is asked.
+The exit atom is displayed, on a single line if possible,
+and the user is prompted with @samp{Valid?}.
+If the atom does not fit on one line,
+the predicate/function name is printed on the first line and
+the arguments are printed one per line
+using the same mechanism that the debugger uses to print values.
+This means they may be abbreviated if they are too large.
+
+For the second type of assertion,
+a ``missing answer'' question is asked.
+The call atom is displayed, prefixed by @samp{Call},
+followed by each of the exit atoms
+(indented, and on multiple lines if need be).
+The user is prompted with @samp{Complete?}.
+Note that the user is not required to provide any missing instance
+in the case that the answer is no.
+(A limitation of the current implementation is that
+it is difficult to browse a specific exit atom.
+This will be addressed in the near future.)
+
+For the third type of assertion,
+an ``unexpected exception'' question is asked.
+The call atom is displayed
+followed by the exception that was thrown,
+and the user is prompted with @samp{Expected?}.
+
+ at node Declarative debugging commands
+ at subsection Commands
+
+At the above mentioned prompts, the following commands may be given.
+Each command can also be abbreviated to just its first letter.
+ at sp 1
+ at table @code
+ at item yes
+Answer that the assertion is correct.
+ at sp 1
+ at item no
+Answer that the assertion is wrong.
+ at sp 1
+ at item skip
+Skip this question and ask a different one if possible.
+ at sp 1
+ at item restart
+Ask the skipped questions again.
+ at sp 1
+ at item browse @var{n}
+Browse the @var{n}th argument before answering.
+ at sp 1
+ at item abort
+End the declarative debugging session and return to
+the event at which the @samp{dd} command was given.
+ at sp 1
+ at item help
+Summarize the list of available commands.
 @end table
+
+ at node Diagnoses
+ at subsection Diagnoses
+
+If the oracle keeps providing answers to the asked questions,
+then the declarative debugger will eventually locate a bug.
+A ``bug'', for our purposes,
+is an assertion about some call which is false,
+but for which the assertions about every child of that call are not false.
+Since this is a two-valued declarative debugger,
+there are three different classes of bugs that can be diagnosed,
+one associated with each kind of assertion @footnote{
+The fact that the debugger is two valued
+is a limitation of the current implementation;
+future plans are to support three-valued declarative debugging,
+meaning that the user will have the option of answering
+``inadmissible'' in addition to ``yes'' and ``no''.
+This will add a fourth class of bug,
+the ``inadmissible call''.}.
+
+Wrong answer assertions lead to a kind of bug we call an ``incorrect contour''.
+This is a contour (an execution path through the body of a clause)
+which results in a wrong answer for that clause.
+When the debugger diagnoses a bug of this kind,
+it displays the exit atom for the event at the end of the contour.
+The program event associated with this bug, which we call the ``bug event'',
+is the exit event at the end of the contour.
+(The current implementation does not yet display a representation
+of which contour was at fault.)
+
+Missing answer assertions lead to a kind of bug we call
+a ``partially uncovered atom''.
+This is a call atom which has some instance which is valid,
+but which is not covered by any of the applicable clauses.
+When the debugger diagnoses a bug of this kind,
+it displays the call atom;
+it does not, however,
+provide an actual instance that satisfies the above condition.
+The bug event in this case is the fail event
+reached after all the solutions were exhausted.
+
+Unexpected exception assertions lead to a kind of bug we call
+an ``unhandled exception''.
+This is a contour which throws an exception
+that needs to be handled but which is not handled.
+When the debugger diagnoses a bug of this kind,
+it displays the call atom
+followed by the exception which was not handled.
+The bug event in this case is the exception event
+for the call in question.
+
+After the diagnosis is displayed, the user is asked to confirm the bug.
+If they choose to confirm the bug,
+they are returned to the procedural debugger
+at the event which was found to be the bug event.
+This allows the user to investigate (procedurally)
+the events in the neighbourhood of the bug, if they desire to do so.
+If they choose not to confirm the bug,
+which implies that some of their earlier answers must have been mistakes,
+they are returned to the event at which the @samp{dd} command was given.
+In future, it is planned that the user will instead have the option of
+revising those of their answers which directly led to the diagnosis,
+but the current implementation doesn't do this yet.
+
+ at c @node Improving the search
+ at c @subsection Improving the search
+
+ at c XXX describe how to mark suspicious subterms, and how this can help.
 
 @c ----------------------------------------------------------------------------
 
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------