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,UTF8 Path: g2news1.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail From: Stephen Leake Newsgroups: comp.lang.ada Subject: Re: Float conversion 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> <77ee8883-ab9f-42c7-94d5-3d85cdc19693@i28g2000yqa.googlegroups.com> Date: Wed, 04 Aug 2010 03:26:59 -0400 Message-ID: <82pqxyu9bw.fsf@stephe-leake.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (windows-nt) Cancel-Lock: sha1:jkKI2OavrgDRsWYmaYh0Ljf+7KA= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@flashnewsgroups.com Organization: FlashNewsgroups.com X-Trace: eeeca4c591640e029e66126270 Xref: g2news1.google.com comp.lang.ada:12842 Date: 2010-08-04T03:26:59-04:00 List-Id: Phil Clayton writes: > On Jul 31, 4:12 pm, Stephen Leake > wrote: >> Clearly to cover all cases, you >> need A < B, A = B, A > B, A < C, etc. > > You make it sound easy... It is easy! This is a very small program; exhaustive testing is appropriate. > Generally, how do you justify that tests 'cover all cases' so giving > you a 100% chance of finding an error? There are three inputs: A, B, C. According to the code, there are three important edge cases for each pair: A < B, A = B, A > B If we assume the floating point hardware is correct, we don't need to worry about any other cases. So that's nine cases to test, total. > 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 = 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. Ok. I agree this is a white box test that is aware of the code. So add another set of conditions: A < 0, A = 0, A > 0. Still a small finite set of tests. >> > 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. >> >> 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! What are you verifying, if not a specification? If the specification is rubbish, what is the point of verifying it? -- -- Stephe