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

[Peter Schachte]

On Fri, Aug 27, 1999 at 05:02:21AM +1000, Fergus Henderson wrote:
> 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.

This is a worthy goal.

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

That makes it *more* reliable.  Better still static contract checking.

>  But if a compiler relies on an assertion of any kind, and
> that assertion is wrong, then the result must be undefined
> behaviour.

... unless the contract is checked, in which case the "defined"
behavior is a compile-time error or a runtime abort.

But now consider the psychology of what you suggest.  Programmers will
pretty quickly realize that contracts give them no speed improvement,
only some extra documentation and mabye some checking.  But if they
instead provide the same information as a promise, it may improve the
efficiency.  So naturally they'll make the promise, and not bother
with the contract.  At best they'll tend to write the same thing
twice, once as a promise and again as a contract (creating a double
maintenance problem).


-- 
Peter Schachte                     Efficiency is intelligent laziness.
mailto:schachte at cs.mu.OZ.AU            -- David Dunham 
http://www.cs.mu.oz.au/~schachte/  
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
--------------------------------------------------------------------------