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: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public From: Karel Th�nissen Subject: Re: Trust but verify (was Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/28 Message-ID: <333B1DF9.18FE@hello.nl> X-Deja-AN: 228885761 References: <332B5495.167EB0E7@eiffel.com> <5giu3p$beb$1@news.irisa.fr> <332ED8AB.21E7@lmtas.lmco.com> <5go8nk$ngf$1@news.irisa.fr> <3332C049.2A0F@lmtas.lmco.com> <5gue93$2md$3@news.irisa.fr> <33383A6F.3A5A@lmtas.lmco.com> <5ha171$dck@flood.weeg.uiowa.edu> <3338AA0A.7A79CB24@eiffel.com> <333AB895.1459@lmtas.lmco.com> Organization: Hello Technologies, Netherlands Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada Date: 1997-03-28T00:00:00+00:00 List-Id: Ken Garlington wrote: > 1. "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." > > Catching this error via automated testing, in the case of Ariane 5, > depends upon two key aspects: > a. That the proper data is available to trigger the exception > during test. This was not available in the case of the > Ariane 5 (see the final report). > b. That the test would have been executed in the proper > manner. The final report states quite clearly that > proper testing was not performed. > Thus, *in the context of the Ariane-5 development*, this > argument fails. I agree. > 2. "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." > > There are many counter-arguments to this point. However, since > you acknowledge explicitly that it is inapplicable to > this case, it fails inherently. I agree. > 3. "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." > > a. This implies that the QA team would have had proper information > to do such checking. As noted above, the final report clearly > states that they would not have such information. The most thorough > manual validation will fail in the face of incomplete data. > This alone invalidates this claim. Yes, one needs the data. But if the integration team would have had the documentation generated from the DBC-like assertions, it would have been clear to them that the correctness/applicability of the software depends on the maximum horizontal speed of Ariane 5 (or of the actual flight path, to be more specific). Isn't it likely then, that they would have asked for it? Would higher levels of management have refused the provision of these data, if the integration team could show the importance of these data? So there is no certainty here that assertions would prevent the disaster, but it would make it less likely, as was claimed by several advocates of the use of DBC. > b. It also implies that the QA team would have done the check. > Putting aside the argument as to whether the Ariane 5 team > was "worth its salt", the report makes it clear that there > was NOT an emphasis on "thorough validation of everything." > Therefore, the assumption made in this point is in error, > further invalidating the claim. What is your point? I feel you are exercising casuistry here. BTW, DBC is not only about writing assertions in the code, it also involves using the analytical results provided by the system. For this reason the support by the language can be so important! Meyer's claim that the crash was avoidable was about the use of DBC ('language and method') and not about the sole use of assertions in the code. So your argument cannot fairly be used as an argument against Meyer's exposition. > c. There is, of course, the issue of scalability. Can a QA team > check that every call satisfies every assertion manually > (remember that automated testing is described in a seperate > argument), for a system of this size? No evidence is given > to support this claim. This further weakens an already dead > claim. Firstly, your argument depends on claims already refuted. Secondly, verification of the code is not a two-valued process. Assertions can sometimes prove correctness, sometimes incorrectness and sometimes neither. Even if we can not prove the absence of contract breaking, we may be able to show the presence of it. In either case, the use of DBC was useful. And in the case of assumptions that regard the operating environment of the software: not the calls need to be checked, but the input to the system. > There is also a general argument for all of these points. Given > that Design by Contract/Eiffel makes it *possible* to specify > the assertion, would the development team have, in fact, > specified the assertion? The final report clearly indicates that > the team felt the assertion could not be violated in practice, > and that this analysis was agreed to at several management levels. > No evidence is given that, in this context, the assertion would > have been written by *this* team. I suspect most development > teams do not introduce assertions they consider impossible to > trigger! As the paper itself notes: "If you have proved that a > condition cannot happen, you are entitled not to check for it. > If every program checked for all possible and impossible events, > no useful instruction would ever get executed!" By extension, > no useful program would ever get *coded*, even if the > extraneous assertions would be suppressed at run-time, if some > decisions were not made about what assertions to include. It seems you do not properly understand the use of assertions and DBC. Apart from there role during testing and execution, DBC and assertions are part of the documentation. It is not necessary to execute them during testing (I would rather do it, though) and execution. So there does not have to be a performance penalty (again, this switching capability is a good argument for having these checks as part of the language). Even if one deems something impossible, it is still an assumption and should therefore be documented with an assertion. What you are saying is something like: 'this is so obvious that there is no need to document it'. Firstly, in mission critical systems things are never obvious and, secondly, leaving out the obvious is not DBC!!! Then your claim that the assumption is not documented is not supported by the Lions-report, to the contrary, it was 'agreed', but obscured by the 'large amount of documentation'. Therefore, it is absurd to suppose that the programming team would not have made use of assertions in an environment of DBC supported with the proper tools or languages. Yes, you are entitled not to *check* an assertion considered impossible to trigger, but you are not entitled to leave it out! Just do not check it in the production system, but do check it during verification and during testing/simulation. Note that this is exactly what Meyer and Jezequel wrote: not _checking_. They did not suggest to refrain from writing or verifying the assertion. > (There are several other general arguments related to the use of > assertions, of course, but advancing such arguments seems > unnecessary at this point.) So do not mention this at all. > So much for the explicit arguments. Now, for what the paper > does NOT say. You state that "...there should... be > simulation, testing, inspections, independent reviews etc...." > and go on to note that the paper does not *deny* this fact. > This, however, is not the issue. If it is not the issue, why bother? > The issue is, does Design by Contract *require* such activities, which > everyone seems to agree are in fact required? Note, again, that the > statement is made that: Mr Meyer has always been very clear about this. Nowhere the suggestion is made that testing etc. can be skipped or weakened. The point of DBC is that it provides an additional technique for obtaining quality software, not an replacement for testing. BTW what did you not mention? It is far too simple to use this kind of default reasoning. Are you a racist just because you did not explicitly deny it? I would not think so :-). > This says that the crash would probably have been avoided > if Design by Contract/Eiffel (DBC) has been used. It does *not* > say that the crash would have been avoided if Design by > Contract/Eiffel has been used, AND IN ADDITION: I do not want to put words in other people's mouth, so _I_ will state it on my behalf: DBC (language and method) indeed would have avoided the crash. Remember what I have written above: DBC is incomplete without the analysis part. > a. That the proper data had been provided in the *system* > specification. Although this is extensively described > in the final report, the DBC paper makes no mention of > it. As noted above, without such data, all arguments in > support of DBC fail. DBC would have triggered the integration team to ask for that data. > b. That DBC would have caused the introduction of the critical > assertion. As quoted above, it in fact implies the opposite: > that "impossible" assertions may not in fact be introduced. ??? > c. That sufficient manual QA would have been done. The paper > does say that proper manual QA should be done. However, > it does not say how DBC supports this activity, either in > terms of educating management to the need for > this activity (a key issue in the Ariane 5 case), or in > terms of proper performance of this activity. (Apparently, > all that is needed is "salt" :) > > d. That sufficient automated verification would have > been done. Here is the paper's statement on testing: Mixing up testing and verification, hmmmm? These may be identical in systems engineering, they are not in software engineering. > "Is it a testing error? Not really... if one can test > more one cannot test all. Testing, we all know, can show > the presence of errors, not their absence. And the only > fully 'realistic' test is to launch..." > > This, to me, is not a particularly strong endorsement of > testing! > > So, clearly, DBC would not have been *sufficient* in this > case. You emphasized this point later in your post (although, > unfortunately, not in the paper): > > So, if there are people who do not consider this a "platitiude" > (as was obviously true for Ariane 5), and such considerations > are essential to the use of DBC, why does the paper not state this > explicitly? Are you joking? Default reasoning. > So, the only argument remaining is: is DBC *necessary* for > the Ariane 5 case? I would say, no. If the proper flight > trajectory had been provided, and the proper test would have > been performed, then the SRI error would have been detected > before launch. Yes, that is true for flight 501. This again is casuistry. Testing would have remedied indeed, but so would verification with DBC. It seems you only rely on testing. But verification can catch bugs that are very difficult to catch with testing. The paper by M&J was one from a software engineering point of view, and an interesting one from that perspective. And 501 is an good illustration of a software engineering pitfall that can be avoided with DBC. > This is noted in the final report. Note that this > is not an issue of 20/20 hindsight; as several people familiar > with such systems have noted, such a test is standard practice. > One could argue that the proper use of assertions would have been > able to more easily isolate and correct the problem, or that some other > system fault might have been detected through the use of DBC, > but both arguments are irrelevant to the subject of the > paper: that DBC would have saved the Ariane 5 from the *specific* > fault which destroyed it. So, if the paper had emphasized that > proper system engineering and verification testing had been done, > it would have further weakened it's own case. It is not > surprising, then, that no such statement is in the paper. ???? should one comment??? > Unfortunately, continuing to claim that the paper answers these > criticisms, without providing any details as to *how* they are > answered, does not provide me with any confidence that your > paper is valid. Perhaps your paper is not directed at practitioners > in the flight controls or inertial reference fields. If so, then > I could understand why you would ignore the arguments made by > those practitioners, such as myself and Mr. White. (Speaking only for myself) I think the paper is directed at a wider audience than only practitioners in flight controls and IR fields. It will help them and others to understand to problems of software reuse. It is not the case that there is a software engineering for flight control and a different software engineering for other disciplines. I appreciate your replies, because they illustrate the complexities of feedback systems, complex closed loop simulations, fail behaviour, etc., but I do not think that they invalidate M&J's claims. > In any case, I have posted these arguments several times without > response. If you do not respond to this post, I will assume that > no response is possible. This is a silly and childish way of exchanging ideas. Maybe you are the one that needs to be convinced :-).