[m-dev.] pre and post conditions

[Mark Anthony BROWN]

Fergus Henderson writes:
> 
> On 25-Jan-2000, Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> > Peter Ross writes:
> > > 
> > In general, when a call terminates with an exception, the "correct thing"
> > is to ask the user about the correctness of that exception.  The possible
> > answers are:
> > 
> > i)	The exception is correct.  This could happen, for example,
> > 	if the exception is meant to be caught higher up in the
> > 	execution tree.
> > ii)	The call is inadmissible (meaning that the exception is
> > 	irrelevant).  This means that the error is in the caller.
> > iii)	The exception is unexpected.  This means that the error is
> > 	in the predicate called.
> > 
> > If the declarative debugger treats your proposed exceptions no
> > differently to other exceptions, then everything should work fine.
> 
> Yes, but can't it do better than that?
> If a precondition fails, can't you assume that the correct
> answer is (ii) the call is inadmissible?

Yes, provided the admissibility declaration is correct (and the code
it calls is correct, etc).  There should be some sort of option
in the analyser to enable this assumption to be made, but if it is
not set, the analyser should be just as suspicious of the
integrity constraints as it is of the program itself.  If the user
answers that the call _is_ admissible, then there is a bug in
the precondition and the analyser should traverse that part of
the tree.  This is precisely what would happen if the DD treats
a transformed program the same as a non-transformed program :-).
This is similar to what I plan to do with mode/inst declarations,
etc. (that is, there will be some sort of options that let the
analyser or oracle assume that these kinds of items are correct).

As far as implementation is concerned, most parts of the DD will treat
the special exceptions as they treat any other exception.  With the
aforementioned option turned on, however, the analyser could be
programmed to recognise when there is a precondition exception
for which there is no child which is the same exception (not counting
the call to throw, if it is traced).  Such a node would be the one
whose precondition failed.  The analyser may then assume the
node is inadmissible without asking the oracle.  (Similarly for
postconditions).

This isn't a really big gain, as far as I can see, since it only
removes one question from the diagnosis.  As I mentioned earlier,
the bigger gain comes from the fact that the execution tree
is much smaller due to early termination.  This means less time
to construct, less memory used, and of course fewer questions asked.

> 
> And if a postcondition fails, can't you at least rule out (i),
> and only ask the user whether the cause is (ii) or (iii)?
> 

Yes, again if you assume that the declarations are correct.

-- 
Mark Brown, PhD student            )O+  |  "Another of Fortran's breakthroughs
(m.brown at cs.mu.oz.au)                   |  was the GOTO statement, which was...
Dept. of Computer Science and Software  |  uniquely simple and understandable"
Engineering, University of Melbourne    |              -- IEEE, 1994
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------