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

[Warwick Harvey]

Peter Ross wrote:
> 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.

Cute.  :-)

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

What if this condition were written:

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

Or is the user just considered stupid for having written it this way?  :-)

I can't think of one right now, but it wouldn't surprise me if there were 
examples like this where one "equivalent" form of the condition would give 
you a good precondition for one mode and another form would give you a good 
precondition for another mode.

Still, maybe that's just "tough" for the user?

Warwick

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