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

[Zoltan Somogyi]

On 23-Aug-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> @@ -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).

We should consider generating all events even with --trace deep by default.

> + 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}.

I don't like "or greater". How about "at trace levels that generate all events,
i.e. at trace levels decl and rep."

> + 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?

The most important effect will (eventually, when we exploit dependency
tracking) be to make the declarative debugger seem much smarter, but that is
not a feature.

> @@ -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}.

This is not really sound advice. Code that is called from decl or rep modules
should really be decl or rep. However, better advice requires the .decldebug
grade, so you may as well leave it as it is for now.

>  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.

I think it would be simpler to say "with any trace level other than none".

> +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.

"represents incorrect program behaviour" is too vague. How about
"that exhibits a bug, e.g. an exit event giving a wrong answer" ?

> +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.

I don't like this. The first sentence states the obvious, and second says
that events are atoms, and it exaggerates the difference between predicates and
functions. How about

Every CALL event corresponds to an atomic goal,
the one printed by the "print" command at the CALL 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,
> +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.

s/following trace events/events at which control leaves a procedure/

> +These assertions may be true or false, depending on whether or not
> +the program's semantics are consistent with what was intended.

Use:

the program's actual semantics are consistent with its intended semantics.

> + at sp 1
> + at table @asis
> + at item EXIT
> +The assertion is that
> +the exit atom is valid in the intended interpretation.

The assertion corresponding to an EXIT event is that ...

> +In other words, the outputs are correct for the given inputs.

In other words, the procedure generates the correct outputs 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.

The assertion corresponding to a FAIL event is that ...

> +In other words, the complete set of answers has been given for that call.

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 are correct answers;
> +some exit atoms may in fact be wrong,
> +but the truth of the assertion is not affected by this.)

... all exit atoms REPRESENT correct answers ...

> + 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.

The assertion corresponding to an EXCP event is that ...

> +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 that 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.

Delete the last comma.

> +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.

... about the VALIDITY of the event for which the @samp{dd} command was given.

Otherwise the next sentence doesn't make sense.

> +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?}.

You shouldn't rely on the order in which types of assertions are introduced.
How about

When seeking to determine the validity of the assertion corresponding to an
exit atom, the declarative debugger prints the atom, on a single line if
possible, and prints the question @samp{Valid?} for the user to answer.

> +For the second type of assertion,
> +a ``missing answer'' question is asked.

Do something similar here.

> +For the third type of assertion,
> +an ``unexpected exception'' question is asked.

And here.

> +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''.}.

Don't mention two- versus three-value debugging; most readers won't know
what you mean. Just say what the current implementation does; you can update
the documentation when you implement three-valued debugging.

> +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.

> +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, ...

> +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.

In the future, users should have the option of ...

Apart from all these suggestions, the change is fine.

Zoltan.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------