[m-dev.] assertions

[Fergus Henderson]

Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> Fergus Henderson writes:
> > Lee Naish <lee at cs.mu.OZ.AU> wrote:
> > > Some general comments:
> > > 
> > > Assertions are a very general concept and a very flexible syntax has
> > > been chosen for them.  For now, they are just used for the accumulator
> > > introduction optimisation, but its likely that in the future they will
> > > be used for various other things (determinism detection, the declarative
> > > debugging oracle, promise_one_solution,...).
> > 
> > I don't think `:- assertion' declarations will be or should be used for
> > determinism detection or as an alternative to promise_one_solution.
> 
> I agree.  Assertions confer knowledge about the _intended_interpretation_
> of the program (atleast, that's how we've been using the term).  They
> don't say anything reliable about the actual implementation --- if they
> did, we wouldn't need debuggers.  If the compiler wants to make an
> optimization based on some assumption that it can't prove, then what
> it requires from the programmer is a *promise* about the actual
> implementation, not an assertion.
...
> The point is that there is a significant difference between "promises"
> about the program, which the compiler can be allowed to rely on, and
> "assertions" about what the program should be.  I think that if the
> compiler is going to do optimizations which rely on the declarations
> without checking them, then they should be called promises rather than
> assertions, and they should come with a warning similar to that in the
> documentation for promise_only_solution/1.
> 
> > `:- assertion' declarations should always remain something that the
> > implementation is free to ignore.  Likewise, `:- assertion' declarations
> > probably won't be useful for the declarative debugger oracle -- I think
> > the declarative debugger oracle would want to make use of specifications,
> > not `:- assertion' declarations. 
> 
> Well, now the meaning of `assertion' has changed ;).  Last year you defined
> a specification as an assertion that completely specifies the semantics.
> Ie, they were both statements about the intended interpretation.  Now
> `:- assertion' is starting to sound more like C's `assert'.

Oops, you're absolutely right -- I've been inconsistent with my terminology.
In this recent thread I was using "assertion" to mean a promise that
the compiler can rely on, whereas in my posts from April last year I
was using it to mean a statement which the compiler was _not_ allowed
to rely on.

> Maybe we should avoid the word `assertion' altogether?
> I am finding it confusing.

A good idea.

I agree with your suggestion that "promise" is a better term to use;
perhaps we can use "assertion" as the generic term that includes all
different kinds of assertions.

In a separate mail I will post a summary of the different kinds of
assertions there are, and what terminology and syntax I think we should
use for them.

> 			*	*	*
> 
> Regardless of what we call it, the assumption seems to have been made
> that what we wish to assert is a valid formula.  For the purposes of
> declarative debugging it is useful to be able to make meta-level
> assertions, such as:
> 
> 	:- assertion valid(F).
> 	:- assertion satisfiable(F).

Isn't that distinction just an issue of quantifiers?
i.e. if `F' is `p(X)', then can't you write those two statements as

	:- assertion all [X] p(X).	% p(X) is valid
	:- assertion some [X] p(X).	% p(X) is satisfiable

?

-- 
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 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------