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

[Ian MacLarty]

On 1 Oct 2004, at 15:21, Peter Ross wrote:

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

Yes, that's exactly one of the ideas I'll be investigating during the 
course of my masters, so watch this space.

Ian.

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