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,FROM_ADDR_WS, 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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: "Joachim Durchholz" Subject: Re: Interresting thread in comp.lang.eiffel Date: 2000/07/19 Message-ID: <8l4u3s$3nvvm$1@ID-9852.news.cis.dfn.de>#1/1 X-Deja-AN: 648309994 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> <8k5alv$1oogm$1@ID-9852.news.cis.dfn.de> <8kl25k$2q7k0$1@ID-9852.news.cis.dfn.de> <8kt18p$36aor$1@ID-9852.news.cis.dfn.de> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300 X-Trace: fu-berlin.de 964033469 3932150 195.190.10.210 (16 [9852]) X-MSMail-Priority: Normal Reply-To: "Joachim Durchholz" Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-19T00:00:00+00:00 List-Id: Ken Garlington wrote: > "Joachim Durchholz" wrote: > > It's dead simple: If physical parameters (like a horizontal bias) > > enter into the specifications, they must be modelled. > > See, you're already in trouble. Horizonal bias is not a "physical > parameter", in this case. It's an _output_ of the SRI, derived from > physical measurements of the environment, not an input. Arrrgh... do you *ever* read what I say elsewhere, or do I have to reiterate the *full* reasoning whenever I deal with you? I assume that the horizontal bias is a physical property, measured by the IRS and returned by the IRS. In that case, the IRS has a contract that relates physical bias and measured bias. (If the IRS has just paper specifications, it's easy enough to translate them to contracts.) The general flight control software somewhere, in some way, retrieves the measured bias from the IRS. Or the IRS spontaneously sends its data, then there's an interrupt routine that will receive that data. In any case, there is some software that uses this data; and the programmer of that line will very likely see the contract. He will also enter this contract into the contract of the software that he, in turn, is writing, so the contract will percolate up the software layers, until it is seen by somebody at a high level who *also* knows the Ariane-5 trajectories. *If* that high-level programmer looks at the details of these contracts, *then* the problem would have been detected. That's a lot of ifs, though none of them is unreasonable given the care that obviously was general in the Ariane project. That's the reason why I say that assertions would have helped to detect the inconsistency, instead of that they would have automatically detected them > From the OBC (the flight > control) side, it's a value coming in from a different system, via a > bus. If it's scaled, then range checks are ineffective (as I noted > in another post). > > > Assertion modelling need > > not restrict itself to statements on values inside a program, so in > > the end you'll get a contract like > > > > OBC_read_value: INTEGER is > > require > > physical_reality.rocket.horizontal_bias <= some_maximum_value > > ensure > > read_value <= 32767 > > end > > > > This is very different from what you write, and clearly spells out > > what the parameters are. > > It's not clear how you are treating > "physical_reality.rocket.horizontal_bias" here. Is it an input to > OBC_read_value? No. It's physical reality. Or, rather, the specification of physical reality. Not computable (except if you program a simulation - and it's a good idea to have a physical_reality feature with contracts if you ever want to write a simulation, this would ensure that the simulation and the flight control software use the same assumptions). > Perhaps if you posted something a little less vague, such as an > Ethernet device driver written in Eiffel, I might be able to see > the utility of your approach... Adding assertions is work that's proportional to the code size, and frankly I have spent much more time on this issue than I care. So, please stop coming forth with proposals how to spend my free time. I know full well what I can do in it. > > This is my last post on this issue. I have just been crossed by Mr. > > Meyer and don't wish to defend his thinking in public anymore. > > OK, although I would hope that you're defending *your own* thinking > as a rule... Done. Though I'm not going to spend more time to convince you. You're one unusually locked-in individual - I see more interest in tearing down the ideas of others than in evaluating these ideas for their usefulness. (I also see an above-average ability to express your own ideas, which is why I've been taking the time, but the effort-to-effect ratio has been degrading, and I don't wish to bore the audience with repetitions to get the points across.) -Joachim -- This is not an official statement from my employer or from NICE. Reply-to address changed to discourage unsolicited advertisements.