Re: Float conversion

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 04 Aug 2010 08:52:40 -0400, Robert A Duff wrote:

> Stephen Leake <stephen_leake@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