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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel - Ariane crash Date: 1997/07/18 Message-ID: <33D02342.C5E@flash.net>#1/1 X-Deja-AN: 257690054 References: <33C835A5.362A@flash.net> <33CC0548.4099@flash.net> <5qitoi$fdv$1@news.irisa.fr> <33CD6512.2404@flash.net> <33CF6B23.9552B339@munich.netsurf.de> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: Joachim Durchholz wrote: > > Ken Garlington wrote: > > > > Jean-Marc Jezequel wrote: > > > At the risk of repeating myself, and reopening a thread beaten to > > death, > > > the all point of design by contract (DBC) is to > > > make this kind of assumptions explicit. > > > > Which would not have happened in the Ariane V case. > > > > > Ariane 5 is just a nice striking example > > > of working with assumptions that are true at a point in time (Ariane > > 4) and no longer > > > later on (Ariane 5). I think we agreed on this previously. > > > > Yes. However, the assumption would not have been documented via an > > Eiffel assertion, > > as I claimed and you/Meyer never refuted (except to exclaim, > > "casuistry!"). > > Maybe nobody put all the relevant parts of the picture together yet. Let > me try to explain: > > An Eiffel assertion serves a dual purpose: > As a run-time check, it is the equivalent of array bounds checking. The > programmer gets hit on his fingers hard and early when he calls a > routine without making sure the preconditions are satisfied, or (less > important to our discussion) writes a routine that violates its > postcondition or the class invariant. > The second purpose is that of documentation. Assertions are an integral > part of a routine's signature, and serve the same purpose as the type > declarations for routine parameters. The only difference is that type > checking can be done at compile time, while assertion checking must be > deferred to run-time (at least with current compiler technology). > > Now imagine we're organizing class docucmentation differently than > usual: All documentation takes the form of source code. Specifications > are made into deferred (abstract) classes, with no routines implemented. > To implement a class, the programmer takes the specification class and > overrides deferred routines with implementations. > In such a scenario, the specification would not have been overlooked. > The restriction on input values might not have been enforced with a > run-time check, but it would have shown up as an (unchecked) assertion. Assuming that someone 1. would have written the check: "Airframe shall comply with Ariane IV flight profile" (try coding that sometime!), and 2. that the reviewer had done this manual check properly amongst all of the other manual checks that a large number of assertions would imply (or, as the final report states: "Given the large amount of documentation associated with any industrial application, the assumption, although agreed, was essentially obscured, though not deliberately, from any external review."), he would have been told "of course the airframe complies with that profile, that's why we don't need to retest!" To quote again from the final report: "The reason for the three remaining variables, including the one denoting horizontal bias, being unprotected was that further reasoning indicated that they were either physically limited or that there was a large margin of safety, a reasoning which in the case of the variable BH turned out to be faulty. It is important to note that the decision to protect certain variables but not others was taken jointly by project partners at several contractual levels." There is no evidence that any trajectory data were used to analyse the behaviour of the unprotected variables, and it is even more important to note that it was jointly agreed not to include the Ariane 5 trajectory data in the SRI requirements and specification." Considerable (although incorrect) thought went into this decision. So, your statement may be true, but it doesn't appear to be relevant. > > AFAIK the restrictions on the flight control software were known, but > buried in some remote document. Tying code and specification together > should have prevented the crash. Since it wasn't flight control software, but inertial reference software, that had the problem, this seems to be an odd statement. More odd is the assumption that system engineers (the ones most likely to know the differences in flight profile) read code before they read documentation. My experience is just the opposite. > > BTW nothing in this discussion has anything to do with object > orientation, or with the many other design decisions of Eiffel. The > point is just that > > ASSERTIONS SHOULD BE A STANDARD PART OF ROUTINE INTERFACES. > > And I can't find anything wrong about that. I can find several things wrong with it, having experience with safety critical systems. > > Regards, > Joachim > -- > Please don't send unsolicited ads.