[m-dev.] assertions

[Mark Anthony BROWN]

Fergus Henderson writes:
> 
> On 09-Jul-1999, 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.

I realise this probably sounds like hair-splitting, but from the point
of view of declarative debugging, it is not.  Assume we have a
predicate foo/1, that we know that foo(a) is true in the intended
interpretation (I), and that we have an assertion that states that
foo/1 has only one solution.  If foo(b) succeeds, then this indicates
a bug within foo (or in something called by foo) --- since either
foo(a) fails or else the assertion is violated.

Instead of having the assertion, say we called

	X = promise_only_solution(foo)

and we got the answer X = b.  This is different to the first case.  We
would need to ask the oracle about the validity of foo(b).  If it is
not true in I, then foo is buggy as before.  If it is, then the bug is
in the line above --- a "broken promise" (ie an inadmissible call).
The difference comes about because promise_only_solution/1 makes a
promise about the interpretation of the program, whereas assertions
are about the _intended_ interpretation.

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'.  Maybe we
should avoid the word `assertion' altogether?  I am finding it confusing.

			*	*	*

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

and so on.  Assertions of the satisfiability of formulas can be useful
for automatically answering oracle queries about missing answers, eg a
formula that says "there should be a solution somewhere in this set".
Also, we are not confined to two-valued logic as we are with
object-level assertions, so there is the possibility of being able to
assert some other important things:

	:- assertion inadmissible(...).

Cheers,
Mark.
-- 
Mark Brown, PhD student            )O+  |  "Another of Fortran's breakthroughs
(m.brown at cs.mu.oz.au)                   |  was the GOTO statement, which was...
Dept. of Computer Science and Software  |  uniquely simple and understandable"
Engineering, University of Melbourne    |              -- IEEE, 1994
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------