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.2 required=5.0 tests=BAYES_00,FROM_WORDY, INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: "Ken Garlington" Subject: Re: Interresting thread in comp.lang.eiffel Date: 2000/07/14 Message-ID: #1/1 X-Deja-AN: 646155887 References: <8ipvnj$inc$1@wanadoo.fr> <8j67p8$afd$1@nnrp1.deja.com> <395886DA.CCE008D2@deepthought.com.au> <3958B07B.18A5BB8C@acm.com> <395A0ECA.940560D1@acm.com> <8jd4bb$na7$1@toralf.uib.no> <8jfabb$1d8$1@nnrp1.deja.com> <8jhq0m$30u5$1@toralf.uib.no> <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de> <3963CDDE.3E8FB644@earthlink.net> <3963DEBF.79C40BF1@eiffel.com> <2LS85.6100$7%3.493920@news.flash.net> <8k5aru$1odtq$1@ID-9852.news.cis.dfn.de> <8k8pk2$20cab$1@ID-9852.news.cis.dfn.de> <_dS95.9945$7%3.666180@news.flash.net> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Complaints-To: abuse@flash.net X-Trace: news.flash.net 963541083 216.215.65.127 (Thu, 13 Jul 2000 21:18:03 CDT) Organization: FlashNet Communications, http://www.flash.net X-MSMail-Priority: Normal NNTP-Posting-Date: Thu, 13 Jul 2000 21:18:03 CDT Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-14T00:00:00+00:00 List-Id: "David K Allen" wrote in message news:BRab5.418$6E.94216@ptah.visi.com... > "Ken Garlington" wrote > > It keeps getting ignored (I suspect because the question can't be > answered), > > but I'll post this example again. The DbC specification for a module is > > given below. I feel fairly confident that this is considered a good > quality > > example by at least one acknowledged Eiffel/DbC expert. > > ;) > > > > > convert (horizontal_bias: INTEGER): INTEGER is > > require > > horizontal_bias <= Maximum_bias > > > > If, as you say, this would cause the project team to go get information > they > > did not already have, then explain what information it would require and > > why. > > > > (My analysis of this DbC specification is in the link noted above). > > First, I don't think the authors intended that this one function would have > prevented the entire disaster. > If they meant that, then I must join you in your critique. > I think they were trying to give an illustration that would convey the > approach of DBC in the context of the disaster. But I can see you were not > impressed . > > Second, as you point out in your critique, the error occurred prior to where > this function would have been used (conversion from FP to Integer). But if > you accept my previous remark, then that is not the point of their example. > I admit they chose poorly if they were intending to persuade you, who have > such a command of the details. > But for conversation sake, and to illustrate the usefullness of DBC, let's > assume that the flaw occured within 'convert' above. Otherwise, I can't > help you see how DBC helps me think and work. As I note in the paper, you can reasonably generate examples where DbC helps. However, the examples provided to date are not, IMHO, germaine to the specifics of the Ariane 5 case. Here's an even more interesting aspect: Given that the author of the proposed contract appears to be showing an example specific to the Ariane 5 case, and given that he _knew_ a priori where the error resided, and given that (he claims) the information provided in the inquiry was sufficient for him to understand the nature of the problem, he STILL BLEW IT. He failed to write a contract that addressed the problem. This should give anyone pause as to the ease of establishing such contracts. More to the point, I have yet to see anyone write an Eiffel contract that _does_ address the Ariane 5 example -- particularly in a portable and readable manner. Again, this is even after we (apparently) fully understand the conditions we're trying to denote. I'm not claiming that it's impossible, but I suspect that it will be more complicated than a one-liner (as the person who posted the "tangent" contract hopefully also discovered :). > Yes, I know - the reason for this jointly agreed decision was cited as > maintaining CPU performance. My only claim is that if DBC were part of the > coding culture, it would have been less likely that that decision would have > been "jointly" agreed to. However, you have to consider that at least some of the "joint" decisions (in particular, the extermely critical one regarding the SRI specification) were quite likely made by personnel that would have been unaware of the software team's decision to use DbC, much less used those contracts in their decision making process. > If I were working on high-risk stuff with a team > of others trained in DBC, I can't see that we would reach a consensus to > ignore the warning of a precondition. It just would not be done without > management overriding us. Again, the part of the statement that reads "a team of others trained in DbC" is critical to the argument. If you are dealing with a software system on a standard hardware platform, where the domain of interest is mostly software-specific, this is reasonably likely. However, the SRI environment (and, more to the point, the rocket environment containing it) is not likely to meet this criteria.