[m-dev.] Re: assertions

[Fergus Henderson]

Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> Lee Naish writes:
> > Mark Anthony BROWN <dougl at cs.mu.OZ.AU> writes:
> > >Assertions confer knowledge about the _intended_interpretation_
> > >of the program (atleast, that's how we've been using the term)
> > 
> > Me too.
...
> 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.  

But *every* entity mentioned in this discussion tells us something
about the intended interpretation.  Program clauses, promises,
specifications, and even user answers to questions from the
declarative debugger are all supposed to be correct in the intended
interpretation.  All of them might be incorrect, though.

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

That is not how the ideal declarative debugger ought to work, IMHO.
Certainly it makes sense for the debugger to make the working assumption
that they are correct.  However, when the debuger gets to the point where
it thinks it has isolated the bug to a particular program clause,
the programmer ought to be able to ask why the debugger thinks this
clause is buggy, and the debugger should then list all the assumptions
that it used to prove that the clause was buggy.  The programmer should
then be able to identify incorrect assumptions and change them.

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

See above.

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

Well, rather than introducing a meta-logical predicate `inadmissible/1'
and allowing that predicate to be used in `:- assertion ...'
declarations, we could instead provide a new kind of declaration
`:- admissable ... when ...', or use some similar kind of annotation
on the pred/func declaration.  This at least ensures that the meta-logical
part is only in the new kind of declaration or annotation, not in
arbitrary places within logic formulae.

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