[m-dev.] Declarative debugger and pre and post conditions

[Peter Schachte]

On Fri, Oct 01, 2004 at 10:21:27PM +1000, Peter Moulder wrote:
> Should `ensure' raise an exception in the case that the predicate
> ultimately fails?  E.g. if list__merge is called with all input
> arguments, where the first two are sorted but not the third, then
> should list__merge silently indicate `false' as in its current
> implementation, or should it raise an exception as it would with the
> proposal in the preceding message?
>
> As Mercury is a logical language, many of the predicates in the standard
> library are documented in terms of `iff', inviting use as a testing
> predicate rather than as an operation producing output.  For the routine
> `set__insert(Set0, X, Set)', it may be tempting to declare `ensure(not
> empty(Set))' (which would indeed be a reasonable postcondition for the
> normal in,in,out mode), but adding such a declaration would reduce the
> usefulness of that predicate when passing Set as input.

OK, I take your point:  there *are* two different kinds of
"requirements."  But I still don't think they need to be specified per
mode.  I'd identify them as:

    1.	Conditions that must hold for a call to be meaningful.  If the
	condition doesn't hold, then the call can't be trusted to do
	anything sensible.  I'll call these expectations.

    2.	Conditions that must hold whenever a call succeeds.  The merge
	example belongs in this category.  I'll call these
	obligations.  I'll use 'requirements' to refer to both
	expectations and obligations.

So I'll revise my proposal to include two directives:

	:- expect merge(L,M,N) => sorted(L), sorted(M).
	:- ensure merge(L,M,N) => sorted(N).

The second of these says that whenever merge(L,M,N) succeeds, we
should ensure that N will be sorted.  If not, there's a problem with
merge/3 and, if checking is enabled, an exception should be thrown.
The compiler can implement this by scheduling this test at the foot of
each clause for merge/3, and if it fails, an exception should be
thrown.  So this makes sense in any mode.

The first says that merge(L,M,N) should only be *called* when
sorted(L) and sorted(M) hold.  If checking is enabled, then those
goals should be (individually) checked as soon as they can be
scheduled, and if either fails, an exception should be thrown.  Note
that, too, makes sense in any mode.  The predicate may fail or throw
an excpetion before generating a binding for L or M which can be
tested, but it is the case that if L or M is bound to a non-sorted
list when merge/3 is called, merge will throw an exception.

>   - Declarative preconditions, similar to one notion of the domain of a
>     function.  The declarative semantics of a predicate `q(X):- r(X).'
>     having declarative precondition p(X) would be
> 
>       all[X] ( not p(X) ; ( q(X) <=> r(X) ) ).
> 
>     in particular, the program must abort rather than let execution
>     depend on the truth of q(X) for values of X s.t. not p(X).
> 
>     Implementations are allowed (but not required) to offer fairly strong
>     completeness guarantees such as using three-valued logic to reduce
>     the occurrence of aborting when not required to by the `must be
>     sound' requirement.

I would argue that if q(X) is ever called with X bound to a value that
does not satisfy p(X), then the program should abort.  My rationale is
that even if some clever scheduling can let q(X) fail without
aborting, the programmer is better off knowing that q/1 can be called
with an unexpected input, rather than proceding in ignorance.  If
there's some test s(X) in the body of the code that may fail, and the
programmer believes it is OK to quietly fail if s(X) fails even when
p(X) fails, then the requirement should be

	:- expect q(X) => (s(X) => p(X)).
or if that looks too confusing
	:- expect q(X) => (p(X) ; \+ s(X)).


On Sun, Oct 03, 2004 at 05:24:33PM +1000, Ian MacLarty wrote:
> I think it's important to seperate out pre and post conditions so it's 
> plain whether these are conditions the caller or the callee should 
> fulfil.

Agreed.  The propsosed expect declaration indicates conditions on the
caller, while ensure indicates conditions on the callee.  Note,
though, that the callee may bind some of its arguments involved in
expectations, in which case it is the callee that is responsible for
the error.  We could change the proposal to say that expectations are
checked at call time only if the arguments are sufficiently
instantiated, but it seems wrong for the predicate to place
expectations on its callers that it does not place on itself.

> I don't see this mechanism being used as a runtime assertion checking 
> mechanism that would throw an exception when a call doesn't satisfy 
> it's pre or post conditions.  I don't think a specification mechanism 
> should change the semantics of the program it's specifying.  Instead 
> the program could be compiled with a --check-conditions flag and the 
> generated executable would run normally, but would produce a report 
> afterwards saying which calls violated their pre and post conditions.  

I guess that would be OK, too, though once the execution has had some
arguments not meet requirements, the behavior of the whole program is
suspect.  So any error reports after the first may well have been
caused by the first, just like C compiler error messages.  More
importantly, if the program actually *does* something, like deleting
files, you probably don't want to continue when you know something is
wrong.  So I do think it's better to just abort when requirements are
not satisfied.

But I don't think aborting changes the semantics, as I'd rather think
of aborting as outside the semantics of the program.  Ie, the
semantics should say what the program will do if it terminates without
aborting.  If it does abort, all bets are off (though I hope it
doesn't recursively delete my home directory before stopping).

In fact, I'd like to take expect and ensure declarations to suggest to
the compiler that it try some compile-time theorem proving to minimize
the number of runtime tests, and to report at compile time when
requirements are sure not to be satisfied.  Perhaps with a certain
switch, it should even report any requirements that cannot be proved
at compile-time.

-- 
Peter Schachte              Re graphics: A picture is worth 10K words -- but
schachte at cs.mu.OZ.AU        only those to describe the picture. Hardly any
www.cs.mu.oz.au/~schachte/  sets of 10K words can be adequately described with
Phone: +61 3 8344 1338      pictures. 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------