[m-rev.] For review: Declarative debugger documentation

[Ian MacLarty]

For review by anyone.

I will commit these changes with my changes to the declarative debugger
in the last diff I posted.

Ian.

Estimated hours taken: 4
Branches: main

Updated user guide with new declarative debugging features.

doc/user_guide.texi
	Added new declarative debugger features such as inadmissible calls
	and subterm marking.

Index: user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.391
diff -u -r1.391 user_guide.texi
--- user_guide.texi	20 Sep 2004 04:50:23 -0000	1.391
+++ user_guide.texi	30 Sep 2004 10:18:10 -0000
@@ -2129,6 +2129,7 @@
 * I/O tabling commands::
 * Parameter commands::
 * Help commands::
+* Declarative debugger commands::
 * Miscellaneous commands::
 * Experimental commands::
 * Developer commands::
@@ -2153,7 +2154,7 @@
 These commands allow you to type in queries (goals) interactively
 in the debugger.  When you use one of these commands, the debugger
 will respond with a query prompt (@samp{?-} or @samp{run <--}),
-at which you can type in a goal; the debugger will the compile
+at which you can type in a goal; the debugger will then compile
 and execute the goal and display the answer(s).
 You can return from the query prompt to the @samp{mdb>} prompt
 by typing the end-of-file indicator (typically control-D or control-Z),
@@ -3200,6 +3201,45 @@
 @end table
 
 @sp 1
+ at node Declarative debugger commands
+ at subsection Declarative debugger commands
+
+ at sp 1
+The following commands relate to the declarative debugger.  See
+ at ref{Declarative debugging} for details.
+ at sp 1
+ at table @code
+ at item dd
+ at c @item dd [--assume-all-io-is-tabled]
+ at c The --assume-all-io-is-tabled option is for developers only. Specifying it
+ at c makes an assertion, and if the assertion is incorrect, the resulting
+ at c behaviour would be hard for non-developers to understand. The option is
+ at c therefore deliberately not documented.
+Starts declarative debugging
+using the current event as the initial symptom.
+ at sp 1
+ at item trust [@var{module-name}|@var{proc-spec}]
+ at kindex trust (mdb command)
+Tells the declarative debugger to trust the given module, predicate or 
+function.  Individual predicates or functions can be trusted by just giving
+the predicate or function name.  If there is more than one predicate or 
+function with the given name then a list of alternatives will be shown.
+If a predicate shares the same name as a module then the predicate name
+should be module qualified to just trust the predicate, otherwise the
+entire named module will be trusted.
+ at sp 1
+ at item trusted
+ at kindex trusted (mdb command)
+Lists all the trusted modules, predicates and functions.  
+ at sp 1
+ at item untrust @var{num}
+ at kindex untrust (mdb command)
+Removes the object from the list of trusted objects.  @var{num} should 
+correspond with the number shown in the list produced by issuing a `trusted'
+command.  
+ at end table
+
+ at sp 1
 @node Experimental commands
 @subsection Experimental commands
 
@@ -3242,38 +3282,12 @@
 @sp 1
 @item save @var{filename}
 @kindex save (mdb command)
-Saves current set of breakpoints and the current set of aliases
-in the named file as a set of @samp{break} and @samp{alias} commands.
-Sourcing the file will recreate the current breakpoints and aliases.
- at sp 1
- at item dd
- at c @item dd [--assume-all-io-is-tabled]
- at c The --assume-all-io-is-tabled option is for developers only. Specifying it
- at c makes an assertion, and if the assertion is incorrect, the resulting
- at c behaviour would be hard for non-developers to understand. The option is
- at c therefore deliberately not documented.
-Starts declarative debugging
-using the current event as the initial symptom.
-For details, see @ref{Declarative debugging}.
- at sp 1
- at item trust [@var{module-name}|@var{proc-spec}]
- at kindex trust (mdb command)
-Tells the declarative debugger to trust the given module, predicate or 
-function.  Individual predicates or functions can be trusted by just giving
-the predicate or function name.  If there is more than one predicate or 
-function with the given name then a list of alternatives will be shown.
-See also `trusted' and `untrust'.
- at sp 1
- at item trusted
- at kindex trusted (mdb command)
-Lists all the trusted modules, predicates and functions.  See also `trust'
-and `untrust'.
- at sp 1
- at item untrust @var{num}
- at kindex untrust (mdb command)
-Removes the object from the list of trusted objects.  @var{num} should 
-correspond with the number shown the the list produced by issuing a `trusted'
-command.  See also `trust' and `trusted'.
+Saves current set of breakpoints, the current set of aliases and the
+current set of objects trusted by the declarative debugger
+in the named file as a set of @samp{break}, @samp{alias} and @samp{trust} 
+commands.
+Sourcing the file will recreate the current breakpoints, aliases and trusted
+objects.
 @sp 1
 @item quit [-y]
 @kindex quit (mdb command)
@@ -3284,7 +3298,6 @@
 End-of-file on the debugger's input is considered a quit command.
 @end table
 
- at sp 1
 @node Developer commands
 @subsection Developer commands
 
@@ -3535,7 +3548,7 @@
 * Oracle questions::
 * Declarative debugging commands::
 * Diagnoses::
- at c * Improving the search::
+* Improving the search::
 @end menu
 
 @node Declarative debugging concepts
@@ -3559,6 +3572,7 @@
 as assertions about the semantics of the program.
 These assertions may be true or false, depending on whether or not
 the program's actual semantics are consistent with its intended semantics.
+
 @sp 1
 @table @asis
 @item EXIT
@@ -3648,6 +3662,14 @@
 followed by the exception that was thrown,
 and prints the question @samp{Expected?} for the user to answer.
 
+In addition to asserting whether a call behaved correctly or not 
+the user may also assert that a call should never have occured in the first
+place, because its inputs violated some precondition of the call.  For example
+if an unsorted list is passed to a predicate that is only designed to work with
+sorted lists.  Such calls should be deemed @emph{inadmissible} by the user. 
+This tells the declarative debugger that either the call was given the wrong
+input by its caller or whatever generated the input is incorrect.
+
 In some circumstances
 the declarative debugger provides a default answer to the question.
 If this is the case, the default answer will be shown in square brackets
@@ -3668,14 +3690,30 @@
 @item no
 Answer that the assertion is wrong.
 @sp 1
+ at item inadmissible
+Answer that the call is inadmissible.
 @item skip
 Skip this question and ask a different one if possible.
 @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 item browse [@var{n}]
+Start the interactive term browser and browse the @var{n}th argument 
+before answering.  If the argument number
+is omitted then browse the whole call as if it were a data term.
+While browsing a @samp{mark} command may be issued to assert that
+the current subterm is incorrect (see @ref{Improving the search}).
+To return to the declarative debugger question issue a @samp{quit}
+command from within the interative term browser.  For more information
+on the use of the interactive term browser see the @samp{browse} command
+in @ref{Browsing commands} or type @samp{help} from within the 
+interactive query browser.
+ at sp 1
+ at item mark [@var{term-path}]
+The @samp{mark} command can only be given from within the interactive
+term browser and asserts that the marked subterm is incorrect.  The 
+debugger uses this information to better direct the bug search.  If no
+argument is given the the current subterm is taken to be incorrect.  If a 
+ at var{term-path} is given then the subterm at @var{tern-path} relative to
+the current subterm will be considered incorrect.
 @sp 1
 @item pd
 Commence procedural debugging from the current point.
@@ -3702,11 +3740,10 @@
 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.
-There are three different classes of bugs that this debugger can diagnose,
+but for which the assertions about every child of that call are not false
+(i.e. they are either correct or inadmissible).
+There are four different classes of bugs that this debugger can diagnose,
 one associated with each kind of assertion.
- at c XXX The preceding comment, and the following discussion, will need to be
- at c updated when we support three-valued debugging.
 
 Assertions about EXIT events
 lead to a kind of bug we call an ``incorrect contour''.
@@ -3740,6 +3777,14 @@
 The bug event in this case is the exception event
 for the call in question.
 
+If the assertion made by an EXIT, FAIL or EXCP event is false and one or
+more of the children of the call that resulted in the incorrect EXIT, FAIL or
+EXCP event is inadmissible, while all the other calls are correct, then an
+``inadmissible call'' bug has been found.  This is a call that behaved
+incorrectly (by producing the incorrect output, failing or throwing an 
+exception) because it passed unexpected input to one of it's children.
+The guilty call is displayed as well as the inadmissible child.
+
 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.
@@ -3763,10 +3808,101 @@
 If the user aborts the diagnosis,
 they are returned to the event at which the @samp{dd} command was given.
 
- at c @node Improving the search
- at c @subsection Improving the search
+ at node Improving the search
+ at subsection Improving the search
 
- at c XXX describe how to mark suspicious subterms, and how this can help.
+The number of questions asked by the declarative debugger before it pinpoints
+the location of a bug can be reduced by giving it extra information.  The kind
+of extra information that can be given and how to convey this information are
+exlained in this section.
+
+ at subsubsection Marking incorrect subterms
+
+An incorrect subterm can be @emph{marked} by the user from within the 
+interactive term browser (see @ref{Declarative debugging commands}).
+The effect of marking a subterm depends on the whether the subterm was part
+of an input or an output argument.
+
+If the subterm was an input then by marking the subterm the user is asserting 
+that the call was inadmissible and that the marked input subterm is the 
+reason for inadmissibility (i.e. the subterm's value violates a precondition
+of the call).
+
+If the subterm was an output then the user is saying the exit atom is false
+in the intended interpretation and the marked subterm is the reason for the
+atom being false (i.e. if it were some other value then the atom would be 
+true).
+
+In either case the next question asked by the declarative debugger will 
+be about the call that bound the incorrect subterm, unless that call was
+eliminated as a possible bug because of an answer to a previous 
+question or the call that bound the subterm was not traced.
+
+For example consider the following fragment of a program that calculates
+payments for a loan:
+
+ at example
+	:- type payment
+		--->	payment(
+				date	:: date,
+				amount	:: float
+			).
+	
+	:- type date ---> date(int, int, int).  % date(day, month, year).
+	
+	:- pred get_payment(loan::in, int::in, payment::out) is det.
+
+	get_payment(Loan, PaymentNo, Payment) :-
+		get_payment_amount(Loan, PaymentNo, Amount),
+		get_payment_date(Loan, PaymentNo, Date),
+		Payment = payment(Date, Amount).
+	
+ at end example
+
+Suppose that get_payment produces an incorrect result and the declarative
+debugger asks:
+
+ at example
+	get_payment(loan(...), 10, payment(date(9, 10, 1977), 10.000000000000).
+	Valid?
+ at end example
+
+Then if we know that this is the right payment amount for the given loan, 
+but the date is incorrect, we can mark the date(...) subterm and the 
+debugger will then ask us about get_payment_date:  
+
+ at example
+	get_payment(loan(...), 10, payment(date(9, 10, 1977), 23.45)).
+	Valid? browse
+	browser> cd 3/1
+	browser> mark
+	get_payment_date(loan(...), 10, dat(9, 10, 1977)).
+	Valid?
+ at end example
+	
+Thus irrelevant questions about get_payment_amount are avoided.
+
+If, say, the date was only wrong in the year part, then we could also have
+marked the year subterm in which case the next question would have been about
+the call that constructed the year part of the date.
+
+ at subsubsection Trusting predicates, functions and modules
+
+The declarative debugger can also be told to assume that certain predicates, 
+functions or entire modules do not contain any bugs.  The declarative
+debugger will never ask questions about trusted predicates or functions.  It
+is a good idea to trust standard library modules imported by a program being 
+debugged.
+
+The declarative debugger must be told which predicates/functions it can trust
+before the @samp{dd} command is given.  This is done using the @samp{trust}, 
+ at samp{trusted} and @samp{untrust} commands at the mdb prompt (see 
+ at ref{Declarative debugger commands} for details on how to use these commands).
+
+Trust commands may be placed in the @samp{.mdbrc} file which contains default
+settings for mdb (see @ref{Mercury debugger invocation}).  Trusted
+predicates will also be exported with a @samp{save} command (see 
+ at ref{Miscellaneous commands}).
 
 @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
--------------------------------------------------------------------------