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

[Peter Ross]

Hi,

I have been thinking about a syntax for pre and post conditions and
think that using the syntax for post-conditions as suggested by Fergus
is adequate

:- check Atom(Vars) => ExecutableFormula(Vars).

This gets around the problem of the pre and post conditions being
dependent on which mode of the predicate is being called, by turning the
pre condition into a post condition (it doesn't matter where the
condition fails).

The pre conditions for a single mode of predicate can then be extracted
by the following process, I believe.
Create a new predicate with the following definition

new(Vars) :-
    ExecutableFormula(Vars),
    Atom(Vars).

Then run mode checking and see which parts of ExecutableFormula are
possible to be left before the call to Atom, and hey presto you have
your pre-condition.

For example the predicate zip(A,B,C) is true iff the list C is the pairs
made up from lists A and B, where the lists A and B must have the same
length.

:- check zip(A,B,C) => (length(A) = length(B), length(A) = length(C)).

:- pred zip(list(T), list(T), list(T)).

:- mode zip(in, in, out) is semidet.
:- mode zip(out, out, in) is semidet.

zip([], [], []).
zip([X|Xs], [Y|Ys], [X-Y|Zs]) :-
    zip(Xs, Ys, Zs).


applying the above algorithm would leave us with 'length(A) = length(B)'
as the pre condition for the mode (in, in, out) and nothing as the pre
condition for the mode (out, out, in).

Counter examples anyone?

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