[m-dev.] Re: assertions (was: Assocative predicates)
fjh at cs.mu.OZ.AU
Fri Apr 24 16:35:06 AEST 1998
On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> > NU-Prolog has a syntax for something like this:
> > :- pred foo(T) where foo(X) : invariant(X).
> > :- pred merge(list(T), list(T), list(T)) where
> > (merge(L1, L2, _) : sorted(L1), sorted(L2)).
> I think syntactically that's not very good; it would be better to stray from
> NU Prolog syntax for this. I think preconditions are much the same sort of
> thing as assertions, and should be syntactically similar.
Well, Lee thinks that preconditions are much the same sort of
thing as types. He has a pretty strong case for it, too ;-)
For example, if the precondition is *not* part of the type of the
arguments, then arguably it would be wrong to write
:- assertion associative_pred(merge).
because merge is not associative for all values of its inputs,
only for the ones that satisfy the preconditions.
Remember that associative_pred is defined as
:- pred associative_pred(pred(T, T, T)).
:- spec associative_pred(P) <=> all [As, Bs, Cs, ABCs]
(P(As, Bs, ABs), P(ABs, Cs, ABCs)) <=>
(P(Bs, Cs, BCs), P(As, BCs, ABCs)).
and here the universal quantifier `all [As, Bs, ...]' is actually
an abbreviation for `all [As in T, Bs in T, ...]'.
Thus the assertion `associative_pred(merge)' is true only
if the type of the argument is `sorted_list(_)', not `list(_)'.
I'm not sure about what is the best way to view preconditions.
In some ways, preconditions seem to me like a fairly operational notion.
In other ways, they seem like a high-level notion, related to 3-valued
interpretations: if a goal's precondition is not satisfied, then that
goal is inadmissable, i.e. the intended interpretation of that goal
is a third truth value "inadmissable".
> > Yes, NU-Prolog also has a syntax for this:
> > :- type sorted_list(T) == list(T) where (X : sorted(X)).
> Perhaps in the interest of consistency, this should be something like
> :- valid_term T => Conditions.
Consistency with what?
I think it may make more sense to consider type invariants to be
parts of types. Considering them to be like assertions
for a special predicate `valid_term' may be straining things a little, IMHO.
> So in summary, here are the new declarations/directives I'd like:
> :- specification Atom <=> Body.
> :- assertion Body.
> :- admissible Atom => Body.
> :- valid_term Term => Body. % or maybe Term::Type => Body.
Which of these, if any, would require the body to be mode-correct?
`admissible' declarations correspond to preconditions, but
there's nothing that directly corresponds to postconditions.
Both specifications and assertions of the form `:- assertion Atom => Body'
could be considered as post-conditions.
It might be better to have seperate declarations (e.g.
`:- precondition Atom => Body' and `:- postcondition Atom => Body')
for assertions that are to be checked at run-time.
I suppose that in addition to postconditions you can also have
a notion of failconditions, to catch goals which should succeed
but instead return no solutions: a specification `Atom <=> Body'
implies a failcondition of `not Atom => not Body' which can be
used for runtime checking.
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 126.96.36.199 | -- the last words of T. S. Garp.
More information about the developers