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: 107d55,a48e5b99425d742a X-Google-Attributes: gid107d55,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public From: jsa@alexandria (Jon S Anthony) Subject: Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/18 Message-ID: #1/1 X-Deja-AN: 226277239 Distribution: world References: <332B5495.167EB0E7@eiffel.com> Organization: PSI Public Usenet Link Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada,comp.lang.java.tech Date: 1997-03-18T00:00:00+00:00 List-Id: In article <5gjoel$jre$1@quasar.dimensional.com> rkaiser@dimensional.com (Richard Kaiser) writes: > In article <332D113B.4A64@calfp.co.uk>, Nick Leaton wrote: > > >2) Design. Writting assertions makes design easier. This is a personal > >observation and harder to justify. I find being clear about what > >something does helps clear up what I am doing. Having complex > >preconditions is not a good idea, again you probably don't have the > >right structure. > > The code is going to assert "I will not run correctly in this new rocket?" No. And this is not the sort of thing that simple pre and post conditions is going to help you with. It's disingenuous to say otherwise. In fact, while this paper is fairly good in its analysis, it is extremely poor in its conclusion. Here's the relevant bit: "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:" Well, the facts indicate that the answer should be "highly UNlikely". Why? Because the language used _does_ have such capabilities. Here's the relevant Eiffel: convert (horizontal_bias: INTEGER): INTEGER is require horizontal_bias <= Maximum_bias ... The *exact* analog with the *exact* same capabilities in Ada is: function Convert ( Horizontal_Bias: Integer ) return Integer is subtype Bias_Constraint is Integer range 0..Maximum_Bias; Require : Bias_Constraint := Horizontal_Bias; ... So, the _only_ evidence we in _fact_ have, is that this sort of capability DOES NOT help in this sort of scenario. And actually, that should not be very surprising. It is not even particularly interesting. Here are a few more bits which just don't hold up: "Assertions (preconditions and postconditions in particular) can be automatically turned on during testing, through a simple compiler option. The error might have been caught then." Exactly the same in Ada, including the above type of constraint. "Assertions can remain turned on during execution, triggering an exception if violated. Given the performance constraints on such a mission, however, this would probably not have been the case." Exactly the same in Ada, including the above type of constraint. "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." Exactly the same in Ada. Assuming you actually _write_ the assertion. "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." Exactly the same in Ada. Assuming the constraint was written. But, the constraint was not written. This despite the fact that the language, Ada, was fully capabale of _explicitly_ expressing the assertion with clear and easily seen demarcated code. Nick sez, > >There are other more complex parts to Eiffels assertion system, in > >relation to inheritance, and soon in relation to parallel processing. Yes, but the bald fact of the matter is, even the most capable aspects of Eiffel assertions are just too rudimentary to be of any use in this sort of scenario. They do not have anything even remotely like the semantic context capabilities needed to address this problem. /Jon -- Jon Anthony Organon Motives, Inc. Belmont, MA 02178 617.484.3383 jsa@organon.com