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

[Peter Schachte]

On Fri, Jul 09, 1999 at 08:33:58AM +0000, Lee Naish wrote:
> Assertions are a very general concept and a very flexible syntax has
> been chosen for them....  sometimes
> specialised assertions/representations are worthwhile.
> ... For the different uses of assertions its
> typically easiest to look for syntactic matches rather that applying a
> FOL theorem prover to the assertions to see if what you are looking for
> is a consequence of the assertions.

I think this is a very important point.  For the optimization you're
doing now, failing to prove the property you're interested in just
means the code won't be as efficient as it could.  But if these
assertions are used as part of verifing declared properties (eg,
declaring mutual exclusion or exaustiveness), then failing to prove
something true means that a valid program won't compile.  Since most
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," otherwise you're demanding too much of
language implementations, and compilation times will be too long.
Also, the argument that "this will only be needed when the property to
be proved depends on assertions, which won't be that often" isn't very
strong, because assertions may be used a fair bit.  Besides, the
compiler will have to try to prove the properties of interest whenever
properties are to be inferred (eg, determinism inference).


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.
And if we do check this sort of assertion and the check fails, it's
probably the assertion that's wrong.

I'm not too happy with this description of the difference.  I think
there must be a crisper distinction to draw here, but I don't see how
to phrase it.  I hope you see what I mean.


-- 
Peter Schachte                     If you think education is expensive, try
mailto:schachte at cs.mu.OZ.AU        ignorance.
http://www.cs.mu.oz.au/~schachte/      -- Derek Blok 
PGP: finger schachte at 128.250.37.3  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------