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

[Peter Ross]

On 25-Jan-2000, Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> 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.
> 
Correct for some reason I was thinking after the call to take, L would
become more instantiated.

> 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).
> 
I know, I was just trying to think of a troublsome declaration.

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