[m-dev.] Re: for review: add parsing/storing of assertions

[Lee Naish]

Peter Schachte <schachte at cs.mu.OZ.AU> writes:

>of the properties we will be interested in will be undecidable, the
>question of how hard the compiler is required to try to prove some
>property becomes important.  I think the right answer to this question
>has to be "not very hard,"

Agreed.

Traditionally some checks are done at compile time and some are done at
runtime.  There is a third time, often ignored, where checking is
performed: debug time.  This is the traditional time that more complex
assertions/assumptions are found to be incorrect.  Note that clauses are
a particular form of assertion which fit this model.  Just as
declarative debugging can find which clause in your program is wrong, it
can be adapted to find which clause or other assertion is wrong as long
as enough information is kept concerning which assertions were used and
how when compiling each clause.  Its not clear how this should be done
with the current declarative debugger architecture (it would be somewhat
easier with a transformation-based debugger I think).

Conceptually, you can add (an instance of) the assertion to the clause
as an extra conjunct.  The extra conjunct is ignored at runtime since we
"know" its valid and should therefore just succeed.  However, at debug
time it should be checked.  I think its probably a good idea for the
compiler to keep track of these dummy calls so ultimately the
declarative debugger will be able to check the assertions.  I suspect
the current method of assertions being temporarily treated as predicates
then the predicate info being thrown away is a mistake.  We should
generate a predicate for each assertion (possibly even allow named
assertions with some suitable syntax) and (in some grades) even
generate code for these predicates (all arguments will be mode in and
the predicates should be semidet - the determinism will require some
fudging where they are used).  It might be worth fleshing out a more
detailed design and implementing the assertion handling part while that
code is fresh.

>There's another issue that should be raised:  should there be only one
>flavor of assertion?  I think there are really two different kinds:
>assertions that specify (part of) the semantics of a predicate or
>function, and assertions about their implementation.  The former are
>the sorts of things one would like to have checked, preferably
>statically, but if not then dynamically.  If the check fails, the
>code is probably buggy.  The latter sort of assertion are really just
>hints to the compiler; if they can be statically checked, so much the
>better, but if not, we should be prepared to trust the programmer.

If there is such a distinction (which I have some doubts about), I would
have thought the implementation-related assertions are the ones the
compiler would have more chance of checking.  If you look at determinism
declarations, for example, you can see them a form of assertion.  At the
high level (semantics) saying a pred is det is an assertion of the
existence and uniqueness of answers for all possible (well typed)
inputs (you can write this down in first order logic).  At the low level
it says something more strict, related to what Prolog people would
describe as choice points (or lack of).  The compiler is able to check
the low level information which allows the high level information to be
inferred.

The kind of assertions (I think) we are currently discussing are about
just the intended interpretation of the predicate (the semantics).

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