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

[Mark Anthony BROWN]

Peter Ross writes:
> 
> :- pred take(int::in, list(int)::in_list_skel, list(int)::out) is semidet.
> 
> :- check admissibility take(N, L, _) => ( N =< length(L) ).

I think this should be a mode error---L is not bound sufficiently
to be passed to length.  So I don't see this as a problem with
your method.

If the first arg of length had mode in_list_skel, then the problem
you mention would not occur.  The goal would indeed be scheduled
at the start (ie, it would become a pre-condition).

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