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

[Peter Ross]

Ian MacLarty wrote:
> +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.
> +

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.

Interested, any plans to implement such an idea?

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------