assertions (was: Assocative predicates)

[Peter Schachte]

On Thu, 23 Apr 1998, Fergus Henderson wrote:

> I'm leaning towards `:- assertion' as a better name than `:- pragma assert':

Agreed, this is much better.  Making it an operator helps, too.

> I think we should also allow `:- specification' (or perhaps `:- spec')
> with the same semantics as `:- assertion' but with an additional
> restriction that the assertion must be of the form `p(Vars) <=> Goal'

And there should only be one specification per pred or func.

> Often the code for a procedure is identical to its specification,
> so probably it would make sense to use the specification as the default
> implementation if there are no clauses for the procedure.

I'm not sure there's value in this.  It might be simpler to consider the
code for a predicate to be the spec if there isn't a separate spec, rather
than vice versa.  It's a smaller change from the current system.  Also see
below.

> On 23-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> > ... I still think there is something to be said for using words people
> > recognize like "associative," "commutative," etc.  Maybe something like
> > 
> > :- pragma assertion(associative_function(F) = (F(A,F(B,C)) = F(F(A,B),C))).
> > :- pragma assertion(associative_predicate(P) = (
> > 	P(A,B,C), P(C,D,E) <=> P(B,C,F), P(A,F,E)
> > ).
> 
> That's a good idea.  However, these "properties" are in many ways similar
> to ordinary predicates, so I'd prefer a syntax that more closely reflected
> this.  Indeed, this could almost be done just using ordinary predicates,
> without introducing any new construct at all:
> 
> 	:- pred associative_function(func(T1, T2) = T3).
> 	:- specification(associative_function(F) <=>
> 			all [A, B, C] (F(A,F(B,C)) = F(F(A,B),C))).
> 
> 	...
> 	:- assertion(associative_function(int:'+'))).

How about just:

	:- spec associative(F) <=> all [A,B,C] F(A,F(B,C)) = F(F(A,B),C).
...
	:- assertion associative(+).

(If this appears in the int module, there should be no need for the module
qualification.  Also, I'd expect the usual overloading resolution to handle
the distinction between associative preds and funcs.) 

> The only problem with this is that the compiler will complain about
> there being no modes for `associative_function'.
> One way of working around this would be to use a "not_reached" mode

I agree with Andrew on this:  this doesn't seem like a good thing to give
users.  But if you take my suggestion of not making specifications stand in
for missing code, you could take a specification without code (and without a
pred declaration) as a pure specification, only usable in specifications and
assertions.  Obviously you can't call it if it doesn't have code.

This also gives me another idea.  So far we've been talking only about
properties of the success set of predicates/functions.  It would also be
really useful to be able to specify the input requirements of a predicate or
function (other than the types and modes).  You might argue that assertions
cover this, but they don't really.  Assertions tell you that if a predicate
succeeds, its arguments have certain properties.  Requirements tell you what
assumptions the programmer has made about the arguments of the predicate,
and calls not satisfying those requirements may lead to "unexpected" 
results.  Eg, merge/3 might expect its input arguments to be sorted, (/)/2
might expects a non-zero second argument, another predicate might expect one
argument to always be larger than another.

	:- admissible merge(A,B,C) => sorted(A), sorted(B), sorted(C).
	:- admissible _/D => \+ D = 0.
	:- admissible p(A,_,B,_) => A > B.

These requirements could be used to great effect by the debugger.  And the
extent to which any of these things could be automatically checked would be
a real boon to software engineering.

Taking this one step further, what I was asking for a few weeks ago was the
ability to make assertions about all instances of a given type.  For
example, the denominator of a rational must always be > 0.  I don't have a
good syntax proposal for this.  It would probably be easier when the code
for named arguments (members, slots, fields, whatever you want to call them)
is put in.  But I do think this would be very useful.


-Peter Schachte               | The secret of being miserable is to have the
mailto:pets at cs.mu.OZ.AU       | leisure to bother about whether you are
http://www.cs.mu.oz.au/~pets/ | happy or not. The cure is occupation.
PGP: finger pets at 128.250.37.3 |     -- George Bernard Shaw