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,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Joachim Durchholz Subject: Re: Safety-critical development in Ada and Eiffel - Ariane crash Date: 1997/07/18 Message-ID: <33CF6B23.9552B339@munich.netsurf.de>#1/1 X-Deja-AN: 257631214 References: <33C835A5.362A@flash.net> <33CC0548.4099@flash.net> <5qitoi$fdv$1@news.irisa.fr> <33CD6512.2404@flash.net> X-Priority: 3 (Normal) Organization: ccn - computer consultant network GmbH Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: 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. 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. 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. Regards, Joachim -- Please don't send unsolicited ads.