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!i28g2000yqa.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Float conversion Date: Mon, 2 Aug 2010 18:07:20 -0700 (PDT) Organization: http://groups.google.com Message-ID: <77ee8883-ab9f-42c7-94d5-3d85cdc19693@i28g2000yqa.googlegroups.com> 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> <82y6cru1lp.fsf@stephe-leake.org> NNTP-Posting-Host: 91.110.204.86 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1280797640 2012 127.0.0.1 (3 Aug 2010 01:07:20 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 3 Aug 2010 01:07:20 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: i28g2000yqa.googlegroups.com; posting-host=91.110.204.86; 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:12815 Date: 2010-08-02T18:07:20-07:00 List-Id: On Jul 31, 4:12=A0pm, Stephen Leake wrote: > Phil Clayton writes: > > =A0 if A < B and A < C > > =A0 then > > =A0 =A0 Y :=3D A; > > =A0 elsif B < C and B < A > > =A0 then > > =A0 =A0 Y :=3D B; > > =A0 else > > =A0 =A0 Y :=3D C; > > =A0 end if; > > > The justification given is > > > =A0 if A is smallest, set Y to A > > =A0 else if B is smallest, set Y to B > > =A0 else C is smallest so set Y to C > > > Unfortunately, the program doesn't work. =A0If 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. =A0(Fortunately the consequences were not > > too serious, though intriguing.) =A0The program fails exactly when A = =3D B > > < C because it returns C, which is not the minimum. > > I am _always_ suspicious of 'and' conditions in nested if/then/else; it > is easy to leave out a case. If this had been written: > > if A < B then > =A0 =A0if A < C then > =A0 =A0 =A0Y :=3D A; > =A0 =A0else > =A0 =A0 =A0 -- =A0A >=3D C > =A0 =A0 ... > > The problem would have been clear from the start. > > > 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. =A0What are the chances of > > having A equal to B? =A0 > > 100%, for a rationally designed test! Justifying that a set of test cases has a 100% chance of finding an error (when not testing all combinations of all input values) will unavoidably involve formal reasoning, similar to that used for formal methods. I was really talking about less formal approaches to testing. > Clearly to cover all cases, you > need A < B, A =3D B, A > B, A < C, etc. You make it sound easy... Generally, how do you justify that tests 'cover all cases' so giving you a 100% chance of finding an error? Note that even if I had test cases that exercise all possible orderings of A, B and C, I am not guaranteed to find an error in an incorrect implementation of Y =3D min {A, B, C}. For example, I could have chosen positive values for A in every test but the program could have contained an extra erroneous condition ... and 0 < A that would have gone undetected. So the tests need to take account of the particular implementation too. > > Where does the original justification go wrong? =A0Well, when talking > > about 'the smallest' there is an implicit assumption being made that > > it is unique. =A0The justification never considers the case when A or B > > is the non-unique smallest. > > And the same error could be made in a formal specification. "formal" > does _not_ mean "complete"! Although I said "formal methods", I use this example to motivate formal verification, not formal specification. Any specification, formal or not, can be a load of rubbish! > > Of course, the correct program just uses "<=3D" instead of "<", > > That would be one way, but it would still require the same detailed > analysis and test. I prefer the exhaustive if/then/else style above. In the absence of any formal verification support, it's probably a good idea to keep things simple like that. Phil