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

[Peter Ross]

On 25-Jan-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 
> Is all that clear?
> 
Yes, and I am convinced that the admissibility should be seperate check.

The only problem that Mark Brown and I came up with is maybe something
like the following could cause problems:

:- pred take(int::in, list(int)::in_list_skel, list(int)::out) is semidet.

:- check admissibility take(N, L, _) => ( N =< length(L) ).

take(N, List, Taken) :-
    (
        N =< 0
    ->
        List = [_ | T],
        take(N-1, List, Taken0),
        Taken = [1 | Taken0]
    ;
        Taken = []
    ).

Now if the only mode available for length is length(in) = out, then the
constraint would be scheduled after the call to take, which could
possibly fail due to the input being inadmissable but the admissibility
check would never occur because L is never instantiated enough to check
it.

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