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.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,9b4538cfeb0c3576 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!c10g2000yqi.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Float conversion Date: Fri, 30 Jul 2010 06:14:49 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <9e669a3b-1013-4bd1-b372-5f7dfa46d083@f42g2000yqn.googlegroups.com> <1q5zc0ais535h$.1jqwfxhj9cflc$.dlg@40tude.net> <4c519968$0$6893$9b4e6d93@newsspool2.arcor-online.net> <1d1txn4x3r5xn.1trm4gx9n87gm$.dlg@40tude.net> <1jo4xj7cntwy1$.1ntf9smcka8vf$.dlg@40tude.net> <1d617940-d138-4b8c-a321-ed23b47431b8@x21g2000yqa.googlegroups.com> <1naf3ekl5k916$.f7ugc92galdz$.dlg@40tude.net> NNTP-Posting-Host: 91.110.164.153 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1280495691 21944 127.0.0.1 (30 Jul 2010 13:14:51 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 30 Jul 2010 13:14:51 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: c10g2000yqi.googlegroups.com; posting-host=91.110.164.153; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15) Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:12714 Date: 2010-07-30T06:14:49-07:00 List-Id: On Jul 30, 9:43=A0am, "Dmitry A. Kazakov" wrote: > On Thu, 29 Jul 2010 18:30:06 -0700 (PDT), Phil Clayton wrote: > > However, just because equality between floating point numbers is a > > dubious concept and should be avoided, it does not mean e.g. "<" and > > "<=3D" are simply interchangeable. =A0Far from it. > > They are almost same. According to the extension principle: > > I1<=3DI2 > > =A0 T (true) if forall x in I1, forall y in I2 =A0x<=3Dy > =A0 F (false) if forall x in I1, forall y in I2 =A0not x<=3Dy > =A0 _|_ (undefined) otherwise > > I1 > =A0 T if forall x in I1, forall y in I2 =A0x =A0 F if forall x in I1, forall y in I2 =A0not x =A0 _|_ otherwise > > The difference comes from _|_ being rendered T for "<=3D" and F for "<" w= hen > I1 and I2 are equal as sets. It would be ill-advised to exploit this > difference without care. Certainly ill-advised, but it can be difficult to know when this difference matters. This gives me the perfect excuse to wheel out one of my favourite examples. It's a great example that I keep coming back to for many reasons. We want a 3-way min function (for integers or reals) that gives Y =3D min {A, B, C} and we are given if A < B and A < C then Y :=3D A; elsif B < C and B < A then Y :=3D B; else Y :=3D C; end if; The justification given is if A is smallest, set Y to A else if B is smallest, set Y to B else C is smallest so set Y to C Unfortunately, the program doesn't work. If you haven't spotted why, it is well worth trying to work it out, perhaps with a few test cases. In fact, this particular error came to various people's attention because it made its way though all stages of a safety-critical software development process. (Fortunately the consequences were not too serious, though intriguing.) The program fails exactly when A =3D B < C because it returns C, which is not the minimum. I often bring this example up to motivate the use of formal methods as it is particularly difficult to find the error through testing, especially when A, B and C are real types. What are the chances of having A equal to B? Furthermore, the program works when e.g. B =3D C < A. (The issue occurred predictably on the real system however, because A and B were set to 0 under certain conditions.) Where does the original justification go wrong? Well, when talking about 'the smallest' there is an implicit assumption being made that it is unique. The justification never considers the case when A or B is the non-unique smallest. Of course, the correct program just uses "<=3D" instead of "<", which is why this example is relevant here: this goes to show that you can't simply interchange "<" and "<=3D" for real types. Furthermore, "<" and "<=3D" should be chosen carefully to avoid inadvertent equality conditions: in this example, using "<" has introduced an equality test in the condition for taking the final else branch: not (A < B and A < C) and not (B < C and B < A) is equivalent to A =3D B or (C <=3D A and C <=3D B) ^^^^^ Finally, this example goes to show that issues resulting from implicit equality conditions can be really hard to spot! Of course, I could have pointed out that e.g. not (A < B or B < A) and not (A <=3D B or B <=3D A) are not the same but nobody is going to make that mistake - I thought a real example would be more valuable. Sorry for the mild digression, hope that was of interest! Phil