[m-dev.] declarative debugging assertions (was Re: [m-rev.] for review: --no-inline-builtins)

[Mark Brown]

On 30-Jan-2003, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> On 30-Jan-2003, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > You know, I think the declarative debugger really ought to by default
> > assume that everything in the standard library is correct.
> > Having the declarative debugger ask you if 1 + 3 = 4 is not a
> > usability improvement!  (Shades of 1984...)

I agree with this.  However, there is a gotcha that we should be wary
of for when three-valued declarative debugging is supported: some library
predicates have entry conditions that must be satisfied, for example,
that a list should be sorted or should contain no duplicates.  For
predicates like this we still need to ask the question, since we don't
know whether the answer should be 'yes' or 'inadmissible'.  Wrongly
assuming that the answer is 'yes' could lead to the wrong class of bug
being reported, and may also allow the oracle to make incorrect
inferences about the intended interpretation.

> I think you can only assume that everything in the library that
> doesn't take a higher-order argument is correct. With abstract
> types, it could be difficult to know what can take a higher-order
> argument. For example, when processing map__lookup, without
> inter-module optimization the compiler couldn't know that the
> type `tree234' isn't a higher-order type.

This is a good point (as is Fergus' point about typeclass methods).

To understand how the standard library should be treated by the declarative
debugger, it is necessary to be clear on what exactly we mean by "correct".
That is, we need to understand exactly what assertions we wish to make
about programs that use the standard library.

There are at least two kinds of assertion that it is useful to make, which
I shall refer to as "oracle assertions" and "analyser assertions".  Oracle
assertions are pieces of knowledge stored in the oracle database which
basically provide answers to questions, thereby avoiding the need to ask
the user anything about a particular subtree of the debugging tree.  That
is, they simplify the debugging task by allowing parts of the debugging
tree to be pruned away.  An example of this behaviour occurs when a
question is repeated and the previous answer is automatically used
without the user being consulted.  Another example of this kind of
assertion is the statement that "any call to int:(+) will produce the
correct results."  Given this assertion, the declarative debugger could
avoid asking any questions about that function and just assume the
answer is 'yes'.

The meaning of the oracle assertion that foo/2 produces correct results
would be as follows:

	i) the clauses which define foo are valid in the intended
	interpretation,

	ii) the clauses of anything directly or indirectly referred to
	by foo are likewise valid, and

	iii) any higher order terms passed to foo are correct.

So if this kind of assertion is made about list__map, for example, and
the program calls list__map but passes a function to it that in fact
contains a bug, then the declarative debugger may report a bug in the
caller of list__map.  This may be considered an inadequate explanation
of the bug, but as long as the declarative debugger explains its
diagnosis by mentioning the assertion that was used, I think this is
acceptable (it should be possible to remove the offending assertion
and start debugging again if the user wishes).

The other kind of assertion, "analyser assertions", are statements about
the validity of certain clauses.  In most cases, these won't provide
automatic answers to questions, but they reduce the size of the
debugging tree in other ways.  Basically, if a node is for a predicate
or function which is known to have valid clauses, then we remove that
node from the debugging tree and attach its children to the parent.
That is, we effectively unfold the definition of the predicate or
function which we know is valid.

The meaning of an analyser assertion that foo/2 has a valid definition
would be a subset of the above meaning:

	i) the clauses which define foo are valid in the intended
	interpretation.

The change which Zoltan is working on (which I discussed with him in
person) will implement oracle assertions.  I have in mind a way to
implement analyser assertions, but the implementation is significantly
more complex than for oracle assertions, so I will need a bit more time 
to think about it and discuss it.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------