[m-dev.] Re: assertions

[Lee Naish]

Mark Anthony BROWN <dougl at cs.mu.OZ.AU> writes:

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

The suggestions which have been aired for declaring that certain things
are mutually exclusive etc are assertions in the general sense.  Whether
or not they should use the `:- assertion' syntax is another matter, as is
whether determinism detection considers `:- assertion's as well as more
specific declarations.

>Assertions confer knowledge about the _intended_interpretation_
>of the program (atleast, that's how we've been using the term)

Me too.

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

I don't really agree with this.  What is this "actual implementation",
exactly?  I presume its essentially the program clauses.  Even if the
':- assertions' are guaranteed to be correct we need debuggers because
the clauses might not be true in the intended interpretation.  Remember,
*clauses are assertions too*.  If all the clauses (or completion) and
all the ':- assertions' are true in the intended interpretation there
should be no problem (modulo termination/completeness).  If any of the
clauses/completion or ':- assertions' are false the program has a bug
which may (or may not) show up when the program is run (and if it does,
we should be able to track it down with a declarative debugger).  I
think this is a very clear, purely declarative way of looking at it.

I suspect other more complex views which try to distinguish assertions
from promises, {actual} implementations from specifications/assertions/
etc stem from the difficulty many people have in viewing program clauses
in a *purely declarative* way.  It is hard for programmers to avoid thinking
of program clauses in a different way to "assertions" (and much of the
time they must be thought of differently).  However, the beauty of
declarative programming is you can step back sometimes and ignore the
procedural reading.  There is then no difference at all between program
clauses and "assertions".

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

There are *two* possible bug diagnoses here:
1) the bug diagnosis of the (unsatisfiable) atom foo(b)
2) the assertion is incorrect

To determine which of these should be reported a debugger needs to know
the validity of foo(b).

>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 second case here is equivalent to the second case above.

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

These can be done using object level formulas with suitable
quantification.

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

True.  However, this (quite rightly) questions the semantics of Mercury
as a whole.  And the best way to talk about inadmissibility is unclear -
perhaps using the meta level is best, perhaps not.  I think its best to
avoid the meta level as a basis for the assertion language if possisble.

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