Float conversion
in [ADA]
|
Prev: What is your preferred VCS?
Next: GPS 2010 for AVR
From: Georg Bauhaus on 3 Aug 2010 06:38 On 03.08.10 03:07, Phil Clayton wrote: >> Clearly to cover all cases, you >> need A < B, A = 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? When {A, B, C} in (machine) Float, I guess "<", "=", and ">" won't tell the whole story in any case? (If they are assumed to mean what they usually mean in "mathematics".)
From: Stephen Leake on 4 Aug 2010 03:26 Phil Clayton <phil.clayton(a)lineone.net> writes: > On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)stephe-leake.org> > 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
From: Stephen Leake on 4 Aug 2010 03:27 Georg Bauhaus <rm.dash-bauhaus(a)futureapps.de> writes: > On 03.08.10 03:07, Phil Clayton wrote: > >>> Clearly to cover all cases, you >>> need A < B, A = 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? > > When {A, B, C} in (machine) Float, I guess "<", "=", and ">" > won't tell the whole story in any case? Why not? Those are the only conditions tested in the code. -- -- Stephe
From: Robert A Duff on 4 Aug 2010 08:52 Stephen Leake <stephen_leake(a)stephe-leake.org> writes: > Phil Clayton <phil.clayton(a)lineone.net> writes: > >> On Jul 31, 4:12�pm, Stephen Leake <stephen_le...(a)stephe-leake.org> >> 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. I wouldn't call that "exhaustive". To me, exhaustive testing means testing every possible input. There are far more than 9. You seem to be using some sort of coverage metric, not exhaustive testing. > According to the code, there are three important edge cases for each > pair: A < B, A = B, A > B I don't understand that. Phil Clayton's example was: if A < B and A < C then Y := A; elsif B < C and B < A then Y := B; else Y := C; end if; (Interesting example, by the way!) There is no explicit test for A=B, nor B=C in that code. So how did you know those should be tested? And why not A=B-epsilon? By the way, putting: pragma Assert (C < B and C < A); after "else" might have made the bug clearer. Or might not. > What are you verifying, if not a specification? You can't formally verify specifications. You can (sometimes) formally verify that the code matches a specification. > If the specification is rubbish, what is the point of verifying it? The problem is, if we have a specification for something more complicated than "min", we don't know whether it's rubbish, and there's no formal way to prove it one way or the other. Anyway, I didn't see any specification for "min" in this thread. We just assume we all know what it means. But how do we know for sure that min(1.0, 1.0, 99.0) is not supposed to return 99.0? "min" is a poor name for such a function, but what if it were something more complicated? And what is "min" supposed to do with NaNs? Probably there's an implicit precondition that none of A,B,C are NaN. - Bob
From: Dmitry A. Kazakov on 4 Aug 2010 10:32
On Wed, 04 Aug 2010 08:52:40 -0400, Robert A Duff wrote: > Stephen Leake <stephen_leake(a)stephe-leake.org> writes: > >> It is easy! This is a very small program; exhaustive testing is >> appropriate. > > I wouldn't call that "exhaustive". To me, exhaustive testing means > testing every possible input. x every possible initial state (some things are stateful. A pipelined CPU pipeline definitely is. We used to ignore that, can we for "exhaustive" testing?) >> What are you verifying, if not a specification? > > You can't formally verify specifications. You can (sometimes) formally > verify that the code matches a specification. Right. (although one could check a specification for being consistent, i.e. allowing at least one implementation) > Anyway, I didn't see any specification for "min" in this thread. > We just assume we all know what it means. But how do we know > for sure that min(1.0, 1.0, 99.0) is not supposed to return > 99.0? "min" is a poor name for such a function, but what > if it were something more complicated? (I think min is OK to denote the lower bound of a subset that belongs to the subset.) > And what is "min" supposed to do with NaNs? NaN? However the interval NaN is unbounded. -Inf does not have the lower bound (no min). +Inf does not have the upper bound (no max). -------------- I think that in any realistic case writing formal specifications and verifying against them, would simpler than writing formal specifications anyway, deriving specifications of a test set from them, showing that these tests would detect any implementation error (exhaustive), implementing these tests, verifying these test against their specifications and finally running all these tests. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de |