Re: Float conversion

[Phil Clayton <phil.clayton@lineone.net>]

On Jul 30, 9:43 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Thu, 29 Jul 2010 18:30:06 -0700 (PDT), Phil Clayton wrote:
> > However, just because equality between floating point numbers is a
> > dubious concept and should be avoided, it does not mean e.g. "<" and
> > "<=" are simply interchangeable.  Far from it.
>
> They are almost same. According to the extension principle:
>
> I1<=I2
>
>   T (true) if forall x in I1, forall y in I2  x<=y
>   F (false) if forall x in I1, forall y in I2  not x<=y
>   _|_ (undefined) otherwise
>
> I1<I2
>
>   T if forall x in I1, forall y in I2  x<y
>   F if forall x in I1, forall y in I2  not x<y
>   _|_ otherwise
>
> The difference comes from _|_ being rendered T for "<=" and F for "<" when
> I1 and I2 are equal as sets. It would be ill-advised to exploit this
> difference without care.

Certainly ill-advised, but it can be difficult to know when this
difference matters.  This gives me the perfect excuse to wheel out one
of my favourite examples.  It's a great example that I keep coming
back to for many reasons.

We want a 3-way min function (for integers or reals) that gives

  Y = min {A, B, C}

and we are given

  if A < B and A < C
  then
    Y := A;
  elsif B < C and B < A
  then
    Y := B;
  else
    Y := C;
  end if;

The justification given is

  if A is smallest, set Y to A
  else if B is smallest, set Y to B
  else C is smallest so set Y to C

Unfortunately, the program doesn't work.  If 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.  (Fortunately the consequences were not
too serious, though intriguing.)  The program fails exactly when A = B
< C because it returns C, which is not the minimum.

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.  What are the chances of
having A equal to B?  Furthermore, the program works when e.g. B = C <
A.  (The issue occurred predictably on the real system however,
because A and B were set to 0 under certain conditions.)

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.

Of course, the correct program just uses "<=" instead of "<", which is
why this example is relevant here: this goes to show that you can't
simply interchange "<" and "<=" for real types.  Furthermore, "<" and
"<=" should be chosen carefully to avoid inadvertent equality
conditions: in this example, using "<" has  introduced an equality
test in the condition for taking the final else branch:

  not (A < B and A < C) and not (B < C and B < A)

is equivalent to

  A = B or (C <= A and C <= B)
  ^^^^^

Finally, this example goes to show that issues resulting from implicit
equality conditions can be really hard to spot!

Of course, I could have pointed out that e.g.

  not (A < B or B < A)

and

  not (A <= B or B <= A)

are not the same but nobody is going to make that mistake - I thought
a real example would be more valuable.  Sorry for the mild digression,
hope that was of interest!

Phil