Re: Papers on the Ariane-5 crash and Design by Contract

[John Hogg <hogg@objectime.com>]

Bertrand Meyer wrote:
> 
> > What does a language need to support Design by Contract? We are told...
> 
> >>>>"For reuse to be effective, Design by Contract is a requirement. Without
> >>>>a precise specification attached to each reusable component --
> >>>>precondition,
> >>>>postcondition, invariant -- no one can trust a supposedly reusable
> >>>>component."
> 
> > I wonder which languages have built-in precondition, postcondition, and
> > invariant statements...
> 
> Eiffel, for one. People have tried adding these constructs to various
> other languages too, although none of these efforts has gained widespread
> acceptance. And of course in Eiffel they are not an add-on but part of the
> language's basic design (the inheritance mechanism, in particular) and
> methodology. It doesn't mean the concepts are worthless for people
> using other languages. If they were, no one besides Eiffel users would
> be paying attention to Design by Contract.
> 
>         (I don't mean to imply that Eiffel's assertions came out of the
>         blue and that no one else has had related ideas. In a recent
>         posting in a different thread I tried to give a reasonable account
>         of the origin of the ideas, going back to the late sixties,
>         and quoted other languages that have
>         integrated neighboring constructs. The only one that is still
>         active to my knowledge is Turing, although I haven't followed
>         its recent developments.)

Unfortunately, Eiffel's assertions are not sufficient to guarantee
black-box behaviour.  In fact, no existing practical object-oriented
language can support reliable precondition/postcondition pairs, and
Eiffel is no exception.

The reason is object aliasing.  If an object can be reached through
two paths from an execution context, then an assertion on one path
can be invalidated by an unseen operation on another path.  One
solution to this is aliasing control, which doesn't exist in any
mainstream language today (although it isn't hard to retrofit).

Interestingly enough, Turing avoids this problem.  Procedral aliasing
is quite different from object aliasing, and Turing programs can be
provably correct (within the accepted formal definition of the term).
However, aliasing issues becomes glaringly obvious when Turing is
extended to Object Turing.

Eiffel is a great leap forward as an attempt to bring provably
correct programming to the masses.  It's better for this than the
alternatives. (At least the OO ones.)  However, don't make the
mistake of believing that its contracts are unbreakable.  You
can have a full set of them and still blow up your rocket.

-- 
John Hogg			    | ObjecTime Limited
Manager, Toolset Applications	    | 340 March Road
mailto:hogg@objectime.com	    | Kanata, Ontario, CANADA K2K 2E4
Voice: +1.613.591.7053		    | +1.800.567.TIME (+1.800.567.8463)
Fax:   +1.613.591.3784		    | http://www.objectime.com/