[m-dev.] Re: assertions

[Mark Anthony BROWN]

Lee Naish writes:
> 
> 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.

Yes.  I mean the declarative semantics of the program clauses.

There is some confusion, caused mainly by us overloading the term
"assertion".  I have been using it to refer to those entities which
tell us something about the intended interpretation.  
The most common usage for a declarative debugger would be to debug a
program with respect to its specifications.  In this case the entities
would be the specifications, or contracts, of the program.  There is
no question of their correctness --- in such a debugging session they
are correct by definition.

Another way the debugger could be used is to debug the specifications
with respect to some other theory.  In this situation the specifications
would be treated like program clauses, and the other theory would be
treated like the specifications were.  This is not significantly
different from the first case --- there is still some theory that is
correct by definition.

In either case, by "assertions" I meant those things which are correct
by definition.  I will use the term "oracle assumptions" from now on,
unless anyone has any better suggestions.

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

In general, I agree.  When it comes to declarative debugging, however,
there is one distinction --- some of these things will be treated
as oracle assumptions, and the rest will be treated as potentially
incorrect.  (Note that this is not so much a difference in what they
*are*, but in how they will be *used*).

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

This is true, if we are talking about assertions in the general sense.
If we are talking about oracle assumptions, then 2) is a contradiction
in terms.

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

What other options are there?

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