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

[Mark Brown]

On 25-Aug-2002, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> On 23-Aug-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > + 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}.
> 
> What features were you thinking of?
> 

I was thinking of term dependency tracking, but I prefer your characterisation
of this as an "effect" so I've change the second sentence (and also a related
sentence just below that point).

> > +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.)
> 
> Likewise, don't mention the display of contours until we can display them.

While the debugger doesn't yet identify the incorrect contour, it does
assert that one exists, so the documentation does need to mention them.
Since the user will probably wonder why we merely state the existence of
an incorrect contour rather than identify it, I think it is worth
pointing out that this is just a temporary limitation.

An alternative is to (temporarily) modify the debugger so that it doesn't
mention contours at all, and then not mention them in the docs.  This would
be fine by me, but it should be in a separate change.

> 
> > +After the diagnosis is displayed, the user is asked to confirm the bug.
> 
> s/confirm the bug/confirm that the event located by the declarative debugger
> does in fact represent a 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.
> 
> If the user does 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.
> 
> If the user does not do so, ...

Unfortunately, this half conflicts with the sentence immediately prior to it
(that is, the sentence in between the two quoted ones).  I've made a
similar change, though:

	If the user does confirm the diagnosis, ...
	If the user does not confirm the diagnosis, ...

I followed your other suggestions.  I'll commit the result now so you
can commit your change that depends on this one; any further review
comments will still be welcome, though.

Cheers,
Mark.

diff -u doc/user_guide.texi doc/user_guide.texi
--- doc/user_guide.texi
+++ doc/user_guide.texi
@@ -1625,15 +1625,21 @@
 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.
+at trace levels that generate all events,
+i.e. at trace levels decl and rep.
 For more details see @ref{Declarative debugging}.
 @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}.
+The declarative debugger is able to use this extra information
+to help it avoid asking unnecessary questions,
+so this trace level has the effect of better declarative debugging
+at the cost of increased executable size.
+ at c XXX The following line is commented out because we don't currently mention
+ at c the effect of this trace level in the declarative debugging section; this
+ at c will change when term dependency tracking is documented:
+ at c For more details see @ref{Declarative debugging}.
 @item shallow
 A procedure compiled with trace level @samp{shallow}
 will generate interface events
@@ -1662,7 +1668,7 @@
 @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,
+you wish to use the full power 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}
@@ -1710,9 +1716,8 @@
 no module can be compiled with trace level @samp{none}.
 
 @strong{Important note}:
-If you are not using a debugging grade, but you compile
-some modules with @samp{--trace shallow}, @samp{--trace deep},
- at samp{--trace decl} or @samp{--trace rep},
+If you are not using a debugging grade, but you compile some modules with
+a trace level other than none,
 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}
@@ -3055,7 +3060,8 @@
 
 The debugger incorporates a declarative debugger
 which can be accessed from its command line.
-Starting from an event which represents incorrect program behaviour,
+Starting from an event that exhibits a bug,
+e.g. an event giving a wrong answer,
 the declarative debugger can find a bug which explains that behaviour
 using knowledge of the intended interpretation of the program only.
 
@@ -3074,17 +3080,11 @@
 @node Declarative debugging concepts
 @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.
+Every CALL event corresponds to an atomic goal,
+the one printed by the "print" command at that event.
+This atom has the actual arguments in the input argument positions
+and distinct free variables in the output argument positions
+(including the return value for functions).
 We refer to this as the @emph{call atom} of the event.
 
 The same view can be taken of EXIT events,
@@ -3093,34 +3093,37 @@
 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
+Using these concepts, it is possible to interpret
+the events at which control leaves a procedure
 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.
+the program's actual semantics are consistent with its intended semantics.
 @sp 1
 @table @asis
 @item EXIT
-The assertion is that
+The assertion corresponding to an EXIT event is that
 the exit atom is valid in the intended interpretation.
-In other words, the outputs are correct for the given inputs.
+In other words, the procedure generates correct outputs
+for the given inputs.
 @sp 1
 @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
+The assertion corresponding to a FAIL event 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;
+In other words, the procedure generates the complete set of answers
+for the given inputs.
+(Note that this does not imply that all exit atoms represent correct answers;
 some exit atoms may in fact be wrong,
 but the truth of the assertion is not affected by this.)
 @sp 1
 @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.
+The assertion corresponding to an EXCP event is that
+the call atom can abnormally terminate with the given exception.
 In other words, the thrown exception was expected for that call.
 @end table
 
@@ -3129,17 +3132,17 @@
 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.
+to the procedural debugger at that event.
 
 @node Oracle questions
 @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,
+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 validity of 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.
@@ -3158,33 +3161,34 @@
 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?}.
+When seeking to determine the validity of
+the assertion corresponding to an EXIT event,
+the declarative debugger prints the exit atom,
+on a single line if possible,
+and prints the question @samp{Valid?} for the user to answer.
 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},
+When seeking to determine the validity of
+the assertion corresponding to a FAIL event,
+the declarative debugger prints the call atom, 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?}.
+(indented, and on multiple lines if need be),
+and prints the question @samp{Complete?} for the user to answer.
 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
+When seeking to determine the validity of
+the assertion corresponding to an EXCP event,
+the declarative debugger prints the call atom
 followed by the exception that was thrown,
-and the user is prompted with @samp{Expected?}.
+and prints the question @samp{Expected?} for the user to answer.
 
 @node Declarative debugging commands
 @subsection Commands
@@ -3224,18 +3228,11 @@
 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''.}.
+There are three different classes of bugs that this debugger can diagnose,
+one associated with each kind of assertion.
 
-Wrong answer assertions lead to a kind of bug we call an ``incorrect contour''.
+Assertions about EXIT events
+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,
@@ -3245,7 +3242,7 @@
 (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
+Assertions about FAIL events 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.
@@ -3256,7 +3253,7 @@
 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
+Assertions about EXCP events 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.
@@ -3266,16 +3263,18 @@
 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,
+After the diagnosis is displayed, the user is asked to confirm
+that the event located by the declarative debugger
+does in fact represent a bug.
+If the user does confirm the diagnosis,
 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,
+This gives the user an opportunity, if they need it,
+to investigate (procedurally) the events in the neighbourhood of the bug.
+If the user does not confirm the diagnosis,
 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
+In the future, users should have the option of
 revising those of their answers which directly led to the diagnosis,
 but the current implementation doesn't do this yet.
 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------