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

[Zoltan Somogyi]

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.

Actually, if you intend to use the declarative debugger, then this
transformation is not necessary. One could instead record the identity
of the precondition and postcondition procedures in the procedure layout,
and make the declarative debugger invoke the precondition at call ports
and the postcondition at exit ports. We could of course provide an mdb
command to make the procedural debugger do so as well.

This scheme has the advantage that you get the overhead of executing the
pre- and postconditions only inside the declarative debugger, and even then
only selectively. (E.g. one could arrange to override the pre- and
postconditions in the program with answers from the oracle). There are
of course offsetting disadvantages: the declarative debugger must perform
an extra check at all call and exit ports, proc layouts become bigger,
and someone must design a mechanism to ensure that postcondition procedures
are passed the right input arguments. (Arranging to pass the right arguments
to the precondition is trivial; neither pre- nor postconditions can have output
arguments.)

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