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

[Fergus Henderson]

[resurrecting an old thread]

On 13-Jul-1999, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> 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.

In the new nomenclature that I recently proposed, both occurrences of
"assertions" above should be "promises", and "specifications" should
be "contracts".

The reason that the compiler should be allowed to rely on promises
but not on contracts is that we want to encourage people who are concerned
about program reliability to add contracts to their programs.
Adding a contract to an existing program should not make it less reliable,
unless run-time contract checking is enabled, and even then in the worst
case you would get a run-time error, not incorrect results or undefined
behaviour.  But if a compiler relies on an assertion of any kind, and
that assertion is wrong, then the result must be undefined behaviour.
So allowing the compiler to rely on contracts would mean that if you
added an incorrect contract, it might cause your program to do the wrong
thing.  That would be undesirable.

Cheers,
	Fergus.

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