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.9 required=5.0 tests=BAYES_00 autolearn=ham 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: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public From: Ken Garlington Subject: Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/31 Message-ID: <33400A09.5572@lmtas.lmco.com> X-Deja-AN: 229665406 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> <3335BC24.13728473@eiffel.com> <3335BE7B.2C67412E@eiffel.com> Organization: Lockheed Martin Tactical Aircraft Systems Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada Date: 1997-03-31T00:00:00+00:00 List-Id: Robert Dewar wrote: > > Bertrand Meyer wrote > > << !! Does this mean that the crash would automatically have > !! been avoided had the mission used a language and method > !! supporting built-in assertions and Design by Contract? > !! Although it is always risky to draw such after-the-fact > !! conclusions, the answer is probably yes:>> > > Note that this conclusion is completely language independent. In particular > the use of assertions is not language dependent. No method can possibly > *rely* on having actual execution of assertions, since that just reduces > you to relying on testing, but certainly execution of assertions is a > helpful adjunct to testing, and certanly at the level that was needed in > this case, any language can certainly implement runtime assertions. If the arguments supplied in support of this argument were limited to run-time execution of assertions, I would agree with this. However, of the three arguments offered, only the first two are related to execution. The third argument, considered the "most important" is as follows: "But most importantly the assertions are a prime component of the software and its documentation ("short form", produced automatically by tools). In an environment such as that of Ariane where there is so much emphasis on quality control and thorough validation of everything, they would be the QA team's primary focus of attention. Any team worth its salt would have checked systematically that every call satisfies the precondition. That would have immediately revealed that the Ariane 5 calling software did not meet the expectation of the Ariane 4 routines that it called." I believe Mr. Meyer considers this a critical distinction between Eiffel and other languages such as Ada. The ability to document assertions explicitly, and have them _read_ as part of the _specification_, appears to be a prime consideration. Consider this Ada example: package X is subtype Value is Float range 1.0 .. 100.0; procedure Update ( New_Value : in Value ); Rate_Error : exception; -- raised when Update changes Contents by more than 5% private Contents : Value := 1.0; end X; As I understand it, the Eiffel way would be to define the Rate_Error condition as an explicit constraint on the Update operation, such as: update ( new_value : INTEGER ) is require abs ((contents - new_value) / contents) > 0.05 do contents := new_value end rather than relying on the comment associated with the exception declaration. This equation would end up in the "short form" version of this declaraion, making it more obvious as to the nature of the assertion. I thought this was at least part of the reason why Mr. Meyer stated that Eiffel and Sather were the only languages that captured the spirit of Design by Contract. The role of exceptions as documentation is emphasized in Mr. Meyer's Introduction to Eiffel at www.eiffel.com: "Run-time checking, however, is only one application of assertions, whose role as design and documentation aids, as part of the theory of Design by Contract, exerts a pervasive influence on the Eiffel style of software development." So, if Design by Contract includes the premise that assertions must be documented in the specification (the "contract") in an explicit manner, then I don't believe this claim can be made for most languages. Certainly, declaring the name of the exception (Rate_Error, in this case) could be argued as an equivalent, but I don't believe Mr. Meyer would agree. > > The main point is that a systematic design using Design by Contract would > indeed probably have avoided the error. However, be careful not to conclude > from this observation that Design by Contract somehow has something special > to say in the Ariane case. > > As has become painfully obvious in the aftermath, the Ariane 5 incident > could have been avoided by any number of means, and almost any competent > design approach, formal or informal, should have prevented this particular > software error. Even in the absence of a systematic design approach, > rigorous testing and/or common sense in approaching the design would have > avoided the problem. I agree. Moreover, it appears to me that the quoted statement claims that there is something special about Design by Contract, *in this particular case* > The Ariane 5 crash was spectacular, and therefore acts as a focus for > discussion, but in fact it is not a particularly instructive example of > a BIG BUG. On the contrary it was the kind of simple minded carelessness > that plagues software, and can be reduced or eliminated without any > very specialized techniques if you have competent people working in a > reasonably systematic manner. -- LMTAS - The Fighter Enterprise - "Our Brand Means Quality" For job listings, other info: http://www.lmtas.com or http://www.lmco.com