Re: Float conversion

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Stephen Leake <stephen_leake@stephe-leake.org> writes:

> Phil Clayton <phil.clayton@lineone.net> writes:
>
>> On Jul 31, 4:12�pm, Stephen Leake <stephen_le...@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