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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: jsa@alexandria.organon.com (Jon S Anthony) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: #1/1 X-Deja-AN: 257514990 Distribution: world References: <33CBBF4B.7BAF@pseserv3.fw.hac.com> <33CC64CE.44A3@flash.net> <5qklt1$4el$2@miranda.gmrc.gecm.com> Organization: PSINet Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: In article <5qklt1$4el$2@miranda.gmrc.gecm.com> paul.johnson@gecm.com (Paul Johnson) writes: > Whilst I don't agree with Meyer that Eiffel would probably have prevented > the Ariane crash Agreed, :-) , he does have a point. No, he does not. Well, actually he does - editors can be fooled into passing off simple advertising for real articles. > The thing is that in Eiffel the assertions are not just a run-time error > detection mechanism, they are also a documentation and specification > mechanism. The Ada assertion was invisible because it was buried in the > implementation of the routine that failed. An equivalent Eiffel routine > (if it were correct) would have had the assertion in its interface, and > so on up to the top level of the software package under discussion. So > anyone reusing the package would have seen the assertion. The Inquiry > specifically commented that the Ada assertion was buried so deeply that > it was effectively invisible to any review. The problems with this view are truly overwhelming. It's hard to even know how to begin or what to say in this sort of informal setting. Here's a sampling: 1. The sort of "assertion" in this specific case could have been explicitly coded as for the "equivalent Eiffel routine". 2. This level of assertion (range constraint) could be specified in the interface of the routine. 3. This level of assertion would be inherited if any types were derived from the type specifying it (just like in Eiffel). 4. So, for this case, Eiffel brings absolutely nothing to the table that wasn't readily available to the Ada programmers. Nothing. Zero. Nada. Zilch. 5. The engineers and programmers knew all about this capability. In fact such an explicit assertion with an attendant exception handler was even in place at one point. 6. The engineers concluded that _for the context of intended use_ (Ariane IV launches) this condition _could not occur_ unless the _physical_ system had catestrophically failed. 7. Like _good_ engineers, this therefore _useless_ explicit check was removed in order to free up some cycles that could be used on something that _was_ worth processing. 8. Such contextual semantics of intended use settings are extremely problematic to codify using standard formal methods (assertions, functional representation, etc. things like Z, LARCH, ZD, etc.). There is even reason to believe that this is not even _possible_, let alone practical. 9. For some reason, many "formal method advocates" still don't get this - despite 15+ years of overwhelming evidence to the contrary. This obstinacy is reminescent of the GOFAI camp who thought all you had to do to get intelligence was hang a frame system (or some other such symbolic representation) off an NL parser. There was a lot of "and Bob's your Uncle" talk coming out of them too. 10. Setting reason aside and attempting to annotate "components" with such ancillary semantic information just results in huge amounts of difficult to manage and typically irrelevant information. The result is the usual "information overload" which can actually tend to _obscure_ real problems. 11. Even trying to come up with the "correct" annotations apriori is an extremely suspect activity. Any given context of use is so overwhelming complex and multifaceted, that trying to codify it by means of such one dimensional micro level detail is a lost cause. This is a lesson that FMs would be wise to take from the knowledge representation school of hard knocks. 12..oo, and on and on... > Where this argument falls down, I'm afraid, is that the package did not > receive its data from another software package, but from a hardware > sensor. At this point the whole idea breaks down. A pity. This doesn't even scratch the surface of why this view is bogus. /Jon -- Jon Anthony OMI, Belmont, MA 02178 617.484.3383 "Nightmares - Ha! The way my life's been going lately, Who'd notice?" -- Londo Mollari