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

[Peter Schachte]

> Could I suggest that a useful feature would be the following.  A pragma 
> which could could give pre and post conditions for a call.
> 
> :- pragma pre_condition(merge_sort(A::in, B::in, C::out),
> 		(sorted(A), sorted(B)).
> 
> This would have the advantage that this inadmissable assertion could be 
> automatically generated.
> 
> It would also allow a useful source to source transformation that could 
> place these pre and post conditions into the code generated and throw an 
> exception whenever a pre and post condition were not valid.

It would seem unfortunate to require the distinction between pre- and
post-conditions in a language that supports multiple modes, because it
requires a lot of redundancy.  How about instead just "requirements,"
which includes both preconditions and postconditions.  Then
requirements would just be goals that are implicitly added to each
clause for the specified predicate.  The compiler would be obliged to
schedule the requirements at the earliest time they could be
scheduled, so requirements that mention only arguments that are inputs
in the current mode would be preconditions, and requirements that
mention outputs would be considered postconditions.  So your example
could be rewritten:

    :- pragma ensure(merge_sort(A, B, C),
                     (sorted(A), sorted(B), sorted(C))).

Then this same sanity checking pragma could be used to ensure the two
inputs are sorted before calling, and verify that the output is sorted
on completion.  But when called in an (out, out, in) mode, it would
verify that the last argument is sorted at call time, and that the
first two arguments are sorted on completion.

I'd also like to see something like this allowed in inline code, so in
a the middle of a particular clause I could add an assertion (In the C
sense) that some arguments have some property.  Maybe I expect a
predicate do_something(X, Y) to only succeed when Y is sorted, at
least given what I know about X.  Then I could write:

	do_something(X, Y),
	ensure(sorted(Y)),
	...

Then as soon as Y becomes ground, the sorted/1 goal is scheduled.  If
it succeeds, great.  If not, an exception is thrown.  If the code is
used in a mode where Y is an input, the sorted/1 goal is scheduled
first.


-- 
Peter Schachte              Nearly all men can stand adversity, but if you
schachte at cs.mu.OZ.AU        want to test a man's character, give him power.
www.cs.mu.oz.au/~schachte/      -- Abraham Lincoln 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------