From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,a48e5b99425d742a X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public From: John Hogg Subject: Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/24 Message-ID: <3337072C.50B@objectime.com>#1/1 X-Deja-AN: 228078685 References: <332B5495.167EB0E7@eiffel.com> <332D113B.4A64@calfp.co.uk> <5gm8a6$2qu$2@news.irisa.fr> <3332BE49.8F9@lmtas.lmco.com> <33330FE5.3F54BC7E@eiffel.com> Organization: ObjecTime Ltd. Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada Date: 1997-03-24T00:00:00+00:00 List-Id: 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/