[m-dev.] syntax for pre and post conditions

[Mark Anthony BROWN]

Peter Ross writes:
> 
> Yes, once you have identified the pre and post conditions, you generate
> code like
> 
> atom(Vars) :-
>     (
>         pre-condition(Vars)
>     ->
>         Atom(Vars),
>         (
>             post-condition(Vars)
>         ->
>             true
>         ;
>             throw(post)
>         )
>     ;
>         throw(pre)
>     ).
> 
> I assume that the declarative debugger could catch the exceptions and do
> the correct thing.
> 

It won't need to catch the exceptions---it will notice the EXCP event
and handle that.  It should be able to do the correct thing, though.
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.
For DD, the advantage of throwing these exceptions is that the
execution tree will be smaller than if execution were allowed to
continue as normal, which means fewer questions to the oracle.

Cheers,
Mark
-- 
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
--------------------------------------------------------------------------