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/16 Message-ID: #1/1 X-Deja-AN: 647112901 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.2919.6600 X-Complaints-To: abuse@flash.net X-Trace: news.flash.net 963784170 216.215.65.111 (Sun, 16 Jul 2000 16:49:30 CDT) Organization: FlashNet Communications, http://www.flash.net X-MSMail-Priority: Normal NNTP-Posting-Date: Sun, 16 Jul 2000 16:49:30 CDT Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-16T00:00:00+00:00 List-Id: "Joachim Durchholz" wrote in message news:8kt18p$36aor$1@ID-9852.news.cis.dfn.de... > 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. 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? It shouldn't be, since the purpose of OBC_read_value is to get this parameter off the bus. So, this makes no sense. Are you saying that this is an output of OBC_read_value (or a mapping to a memory-mapped variable)? This is correct, although I thought that the "ensure" statement was the one that was enforced as a post-condition, whereas "require" was a precondition. If "require" statements are enforced on output (or on access to memory-mapped values), then the only problem is that "some_maximum_value" is ALWAYS 32,767. That's what scaling does: It converts floating-point numbers to a scaled integer value, typically using the maximum precision available (that is, the smallest floating point number expected is converted to -32,768, and the largest expected value is converted to 32,767, at least for a 16-bit bus as in the case of Ariane 5). Therefore, all your "require" or "ensure" contract says is that the bus is a 16-bit bus. This is useful if the architecture changes, and the bus grows (or shinks, although this is unlikely) in bit width. However, it has absolutely no utility in checking individual bus parameters. In other words, your contracts will always pass, so long as the bus stays the same. If scaling were not used, then your contract would potentially have more value. However, if scaling weren't used, then the specific error encountered by the SRI would have been avoided. The SRI was in the act of scaling horizonal_bias to put it on the bus when the overflow occured. (The word "expected" in the paragraph above is key to understanding the problem.) 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... > 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. > > Regards, > Joachim OK, although I would hope that you're defending *your own* thinking as a rule...