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

[Fergus Henderson]

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

Run-time checking at development time certainly makes programs more
reliable.  Run-time checking at program ship time is a mixed blessing,
though -- generally it does improve reliability overall, but occaisionally
it causes spurious failures due to incorrect checks.

For example, someone recently reported a bug in the Mercury compiler
where it failed with a software error.  The fix was to change a call
to `map__det_update' with `map__set'.  `map__det_update' is basically a 
version of `map__set' with extra error checking, and in this case the
extra checking was a mistake.

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

Compilers are free to rely on contracts which are run-time checked,
so long as they only rely on the condition _after_ the condition has been
checked.  After all, in that case they are not really relying on the
condition, because the code that they generate will correctly handle
the case where the condition is false.

This is not the same thing as treating a contract as a promise.
Note that if you write something as both a promise and a run-time checked
contract, then the compiler is free to optimize away the run-time check!

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

Not necessarily -- that depends on their aims.

Contracts only provide extra documentation and possibly extra checking.
If programmers aren't interested in that, they shouldn't use them.
But good software engineers usually are interested in such things.

Promises may increase efficiency, but they do so at the expense of
decreasing reliability.  Furthermore they can potentially cause problems
with portability, because bugs may occur with one implementation but
not with another (and likewise for efficiency).

People who are focussed on efficiency to the exclusion of all else
might always use promises rather than contracts.  But such people
won't be using Mercury in the first place ;-).

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

I don't think there's much point in writing something as both a promise
and again as a contract.  It suffices to just write the promise;
the corresponding contract is implied.

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