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

[Peter Schachte]

On Tue, Jul 13, 1999 at 12:45:28PM +1000, Fergus Henderson wrote:
> I agree, although I would put it slightly differently: we want
> both "assertions", that the compiler is allowed to rely on, and
> "specifications", that the compiler is not allowed to rely on but is
> allowed to check.

Not to split hairs any more finely than they've already been split,
but I don't see why the compiler shouldn't be entitled to rely on
specifications.  If anything, I'd expect specifications to be more
reliable than assertions.  And I think it makes some sense for
compilers, in the right ultra-conservative debugging grade, to
generate checks of assertions.  As far as I can see, the real
difference is in "presumption of guilt" when the assertion or
specification is inconsistent with the code.  The other difference is
that specifications are probably put there as documentation, and in
the hope that the will be checked, either statically or dynamically.

> (petdr's current set of changes are only adding support for assertions,
> not for specifications.)

I believe the two sorts of information are closely related, so I think
it makes sense to think ahead a little here and make sure the
infrastructure is compatible with both.

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