Float conversion

Float conversion

[Henrique]

Hi,

I have some problems in converting float variables in Ada. Look at the
code below.

Why var4 is not equal var1?

Thanks.

--
Execution results:
--

var3: =
var4: >

--
Code:
--

with Ada.Text_IO, Ada.Float_Text_IO;
use Ada.Text_IO, Ada.Float_Text_IO;

procedure Test is

  type My_Float is digits 6;

  CONVERSION_CONSTANT  : constant My_Float := 6076.11;
  CONVERSION_CONSTANT2 : constant My_Float := 1.0 /
CONVERSION_CONSTANT;

  package Float_Text_IO is new Ada.Text_IO.Float_IO (Long_Float);
  use Float_Text_IO;

  var1: My_Float := 999.9;
  var2: My_Float := var1*CONVERSION_CONSTANT;
  var3: My_Float := var2/CONVERSION_CONSTANT;
  var4: My_Float := var2*CONVERSION_CONSTANT2;
begin
  Put("var3: ");
  if var3 = var1 then
    Put("=");
  elsif var3 > var1 then
    Put(">");
  else
    Put("<");
  end if;

  New_Line;
  Put("var4: ");
  if var4 = var1 then
    Put("=");
  elsif var4 > var1 then
    Put(">");
  else
    Put("<");
  end if;
end Test;

Re: Float conversion

[Jacob Sparre Andersen]

Henrique <henriquemagalhaes@gmail.com> wrote:

> Why var4 is not equal var1?

>   type My_Float is digits 6;
>
>   CONVERSION_CONSTANT  : constant My_Float := 6076.11;
>   CONVERSION_CONSTANT2 : constant My_Float := 1.0 / CONVERSION_CONSTANT;
>
>   var3: My_Float := var2/CONVERSION_CONSTANT;
>   var4: My_Float := var2*CONVERSION_CONSTANT2;

Basically because the relative precision of My_Float is limited to 1e-6.

In general "=" does not make much sense for floating point types.

Cheers,

Jacob
--
Jacob Sparre Andersen Research & Innovation
Vesterbrogade 148K, 1. th.
1620 K�benhavn V
Danmark

Phone:    +45 21 49 08 04
E-mail:   jacob@jacob-sparre.dk
Web-sted: http://www.jacob-sparre.dk/

Re: Float conversion

[Dmitry A. Kazakov]

On Thu, 29 Jul 2010 05:23:42 -0700 (PDT), Henrique wrote:

> I have some problems in converting float variables in Ada. Look at the
> code below.
> 
> Why var4 is not equal var1?

Because they are not. Floating-point operations are inexact.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Georg Bauhaus]

On 29.07.10 14:23, Henrique wrote:

>   package Float_Text_IO is new Ada.Text_IO.Float_IO (Long_Float);

(Any reason you didn't instantiate with My_Float?)


For illustration, inserting Put(Var3, Aft => 15) and
Put(Var4, Aft => 15), I get

$ ./test_fpt
var3:  9.999000244140625E+02=
var4:  9.999000854492188E+02>

Choosing 15 digits instead of 6 in the type definition, I get

$ ./test_fpt
var3:  9.999000000000000E+02=
var4:  9.999000000000001E+02>

There is always a FPT computation that isn't giving the exact
result, since there aren't enough bits for doing real math on
any computer, if you try hard enough.

Georg

Re: Float conversion

[Georg Bauhaus]

On 29.07.10 14:46, Dmitry A. Kazakov wrote:
> On Thu, 29 Jul 2010 05:23:42 -0700 (PDT), Henrique wrote:
> 
>> I have some problems in converting float variables in Ada. Look at the
>> code below.
>>
>> Why var4 is not equal var1?
> 
> Because they are not. Floating-point operations are inexact.
> 

Interestingly, a quick rewrite to C translated with gcc gives a different
impression (of equality),

#include <stdio.h>

int main()
{
  typedef float My_Float;


#define CONVERSION_CONSTANT 6076.11
  const My_Float CONVERSION_CONSTANT2 = 1.0 / CONVERSION_CONSTANT;


    My_Float Var1 = 999.9;
    My_Float Var2 = Var1*CONVERSION_CONSTANT;
    My_Float Var3 = Var2/CONVERSION_CONSTANT;
    My_Float Var4 = Var2*CONVERSION_CONSTANT2;

    fputs("var3: ", stdout); printf("%.15f", Var3);
    if (Var3 = Var1)
      fputs("=", stdout);
    else if (Var3 > Var1)
      fputs(">", stdout);
    else
      fputs("<", stdout);

    fputs("\n", stdout);
    fputs("var4: ", stdout); printf("%.15f", Var4);
    if (Var4 = Var1)
      fputs("=", stdout);
    else if (Var4 > Var1)
      fputs(">", stdout);
    else
      fputs("<", stdout);


    fputs("\n", stdout);
    return 0;
}


$ ./a.out
var3: 999.900024414062500=
var4: 999.900085449218750=

Re: Float conversion

[Georg Bauhaus]

On 29.07.10 17:08, Georg Bauhaus wrote:

>     if (Var3 = Var1)

Ouuuch!

Re: Float conversion

[Dmitry A. Kazakov]

On Thu, 29 Jul 2010 17:08:24 +0200, Georg Bauhaus wrote:

> On 29.07.10 14:46, Dmitry A. Kazakov wrote:
>> On Thu, 29 Jul 2010 05:23:42 -0700 (PDT), Henrique wrote:
>> 
>>> I have some problems in converting float variables in Ada. Look at the
>>> code below.
>>>
>>> Why var4 is not equal var1?
>> 
>> Because they are not. Floating-point operations are inexact.
> 
> Interestingly, a quick rewrite to C translated with gcc gives a different
> impression (of equality),
> 
[...] 
> 
> $ ./a.out
> var3: 999.900024414062500=
> var4: 999.900085449218750=

with Ada.Text_IO;  use Ada.Text_IO;
procedure Test is
  type My_Float is digits 6;

  CONVERSION_CONSTANT  : constant My_Float := 6076.11;
  CONVERSION_CONSTANT2 : constant My_Float := 1.0 / CONVERSION_CONSTANT;

  var1: My_Float := 999.9;
  var2: My_Float := var1 * CONVERSION_CONSTANT;
  var3: My_Float:= var2 / CONVERSION_CONSTANT;
  var4: My_Float := var2 * CONVERSION_CONSTANT2;
begin
  Put_Line ("var1" & Long_Float'Image (Long_Float (Var1)));
  Put_Line ("var4" & Long_Float'Image (Long_Float (Var4)));
end Test;
------------------------
var1 9.99900024414063E+02
var4 9.99900085449219E+02

When rounded to 6 decimal digits both are same. But the underlying base
binary type is longer than 6 digits.

P.S. It is always useful to think of floating point numbers as intervals
(which they are) rather than numbers.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Warren]

Dmitry A. Kazakov expounded in news:1q5zc0ais535h$.1jqwfxhj9cflc$.dlg@
40tude.net:

> On Thu, 29 Jul 2010 05:23:42 -0700 (PDT), Henrique wrote:
> 
>> I have some problems in converting float variables in Ada. Look at the
>> code below.
>> 
>> Why var4 is not equal var1?
> 
> Because they are not. Floating-point operations are inexact.

I.e. "... inexact for _all_ numbers".

Some fractions do express themselves exactly in binary
(like 0.5).

That is why it may "seem" to work some of the time ;-)

Warren

Re: Float conversion

[Jeffrey R. Carter]

On 07/29/2010 07:56 AM, Georg Bauhaus wrote:
> On 29.07.10 14:23, Henrique wrote:
>
>>    package Float_Text_IO is new Ada.Text_IO.Float_IO (Long_Float);
>
> (Any reason you didn't instantiate with My_Float?)

Since it's not used, it doesn't matter what it's instantiated with.

-- 
Jeff Carter
"Drown in a vat of whiskey. Death, where is thy sting?"
Never Give a Sucker an Even Break
106

Re: Float conversion

[Henrique]

On Jul 29, 12:35 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> ------------------------
> var1 9.99900024414063E+02
> var4 9.99900085449219E+02
>
> When rounded to 6 decimal digits both are same. But the underlying base
> binary type is longer than 6 digits.
>
> P.S. It is always useful to think of floating point numbers as intervals
> (which they are) rather than numbers.
>
> --
> Regards,
> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de

As I declared the type with 6 digits, I expected that it would make
the comparison only for these digits (this would gave var4 = var1).

Do I always need to manually truncate the float number to the number
of desired digits before making a comparison of them?? So what is the
advantage of declaring it as "digits 6"?

Thanks

Re: Float conversion

[Jeffrey R. Carter]

On 07/29/2010 11:21 AM, Henrique wrote:
>
> As I declared the type with 6 digits, I expected that it would make
> the comparison only for these digits (this would gave var4 = var1).

"digits N" means the compiler will use at least Ceiling (N * log2 (10) ) bits 
for the mantissa, 'Image will produce a string with N digits, and an 
instantiation of Ada.Text_IO.Float_IO will output N digits by default. There was 
an effect on the minimum size of the exponent in Ada 83, but I don't think that 
applies any more. (There are probably other cases as well where the "digits" 
value has an effect that I can't think of at the moment.) But all operations, 
including comparisons, take place in the underlying implementation or with 
greater precision.

Most x86-type processors have HW floating-point types that correspond to digits 
7, 15, and 18 (IIRC), so on such a machine you should expect your compiler to 
choose one of those. All computations are done using the digits-18 
representation, so there doesn't seem to be much reason to choose another 
representation.

-- 
Jeff Carter
"Well, a gala day is enough for me. I don't think
I can handle any more."
Duck Soup
93

Re: Float conversion

[Dmitry A. Kazakov]

On Thu, 29 Jul 2010 11:21:52 -0700 (PDT), Henrique wrote:

> On Jul 29, 12:35�pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> ------------------------
>> var1 9.99900024414063E+02
>> var4 9.99900085449219E+02
>>
>> When rounded to 6 decimal digits both are same. But the underlying base
>> binary type is longer than 6 digits.
>>
>> P.S. It is always useful to think of floating point numbers as intervals
>> (which they are) rather than numbers.
>>
>> --
>> Regards,
>> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de
> 
> As I declared the type with 6 digits, I expected that it would make
> the comparison only for these digits (this would gave var4 = var1).

No, the underlying base type is more or less free compiler choice. There
are certain rules, which in essence guarantee you accuracy of the basic
operations within the precision specified.

> Do I always need to manually truncate the float number to the number
> of desired digits before making a comparison of them??

You should never use equality or inequality for floating-point types. They
do not have "physical" sense. As I said, floating-point numbers are
intervals. Two non-zero length [independent] intervals are *always*
unequal, even if their bounds are equal.

> So what is the advantage of declaring it as "digits 6"?

That the compiler guarantees you 6 decimal digits accuracy independently on
whatever hardware you have. The idea behind of Ada numeric types is machine
independence. You specify your requirements on the precision and range and
the compiler either gives you what you wanted or else rejects the program.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Phil Clayton]

On Jul 29, 8:15 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> You should never use equality or inequality for floating-point types.

Inequalities (<, <=, >, >=) are ok - I think you meant don't use 'not
equals' (which is still an equality operator).

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.

Phil

Re: Float conversion

[Dmitry A. Kazakov]

On Thu, 29 Jul 2010 18:30:06 -0700 (PDT), Phil Clayton wrote:

> On Jul 29, 8:15�pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> You should never use equality or inequality for floating-point types.
> 
> Inequalities (<, <=, >, >=) are ok - I think you meant don't use 'not
> equals' (which is still an equality operator).

Yes I did, thanks for correction.

> 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.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Phil Clayton]

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

Re: Float conversion

[Henrique]

Thanks for the help (everyone). By using this concept of intervals, I
made the modifications in my code to solve the problem.

On 29 jul, 16:15, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Thu, 29 Jul 2010 11:21:52 -0700 (PDT), Henrique wrote:
> > On Jul 29, 12:35 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> > wrote:
> >> ------------------------
> >> var1 9.99900024414063E+02
> >> var4 9.99900085449219E+02
>
> >> When rounded to 6 decimal digits both are same. But the underlying base
> >> binary type is longer than 6 digits.
>
> >> P.S. It is always useful to think of floating point numbers as intervals
> >> (which they are) rather than numbers.
>
> >> --
> >> Regards,
> >> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de
>
> > As I declared the type with 6 digits, I expected that it would make
> > the comparison only for these digits (this would gave var4 = var1).
>
> No, the underlying base type is more or less free compiler choice. There
> are certain rules, which in essence guarantee you accuracy of the basic
> operations within the precision specified.
>
> > Do I always need to manually truncate the float number to the number
> > of desired digits before making a comparison of them??
>
> You should never use equality or inequality for floating-point types. They
> do not have "physical" sense. As I said, floating-point numbers are
> intervals. Two non-zero length [independent] intervals are *always*
> unequal, even if their bounds are equal.
>
> > So what is the advantage of declaring it as "digits 6"?
>
> That the compiler guarantees you 6 decimal digits accuracy independently on
> whatever hardware you have. The idea behind of Ada numeric types is machine
> independence. You specify your requirements on the precision and range and
> the compiler either gives you what you wanted or else rejects the program.
>
> --
> Regards,
> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de- Ocultar texto das mensagens anteriores -
>
> - Mostrar texto das mensagens anteriores -

Re: Float conversion

[Dmitry A. Kazakov]

On Fri, 30 Jul 2010 06:14:49 -0700 (PDT), Phil Clayton wrote:

> Certainly ill-advised, but it can be difficult to know when this
> difference matters.

I think it could when intervals were used as keys in some sorted map. I
learnt a couple of quite painful lessons when used keys (not intervals
though), which appeared ordered to me, but in reality "<" was not
transitive.

> 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

A great example. I think every programmer wrote something like above at
least once.

[...]

> 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.

Absolutely. Same happens when a poor "<" is used for sorting. It is very
difficult to detect the problem through blind testing. The thing is so
nasty that it can easily pass a branch coverage test.

People overestimate the power of testing, because they often have a mental
model where the behavior is monotonic. They test for the extremes and
consider the rest granted. Your example shows how wrong this presumption is
already in apparently "trivial" cases.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Stephen Leake]

Phil Clayton <phil.clayton@lineone.net> writes:

>   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 am _always_ suspicious of 'and' conditions in nested if/then/else; it
is easy to leave out a case. If this had been written:

if A < B then
   if A < C then
     Y := A;
   else
      --  A >= C
    ...

The problem would have been clear from the start.

> 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?  

100%, for a rationally designed test! Clearly to cover all cases, you
need A < B, A = B, A > B, A < C, etc.

> 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"!

> Of course, the correct program just uses "<=" instead of "<", 

That would be one way, but it would still require the same detailed
analysis and test. I prefer the exhaustive if/then/else style above.

-- 
-- Stephe

Re: Float conversion

[Phil Clayton]

On Jul 31, 4:12 pm, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> Phil Clayton <phil.clay...@lineone.net> writes:
> >   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 am _always_ suspicious of 'and' conditions in nested if/then/else; it
> is easy to leave out a case. If this had been written:
>
> if A < B then
>    if A < C then
>      Y := A;
>    else
>       --  A >= C
>     ...
>
> The problem would have been clear from the start.
>
> > 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?  
>
> 100%, for a rationally designed test!

Justifying that a set of test cases has a 100% chance of finding an
error (when not testing all combinations of all input values) will
unavoidably involve formal reasoning, similar to that used for formal
methods.

I was really talking about less formal approaches to testing.


> 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?

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.


> > 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!


> > Of course, the correct program just uses "<=" instead of "<",
>
> That would be one way, but it would still require the same detailed
> analysis and test. I prefer the exhaustive if/then/else style above.

In the absence of any formal verification support, it's probably a
good idea to keep things simple like that.

Phil

Re: Float conversion

[Shark8]

On Aug 2, 7:07 pm, Phil Clayton <phil.clay...@lineone.net> wrote:
> On Jul 31, 4:12 pm, Stephen Leake <stephen_le...@stephe-leake.org>
> wrote:
>
>
> Any specification,
> formal or not, can be a load of rubbish!
>
> Phil

You are absolutely right, just look at: Unix, Linux, C, C++, X, Perl,
OpenGL's enumeration, etc.

Re: Float conversion

[Georg Bauhaus]

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".)

Re: Float conversion

[Stephen Leake]

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. 

> 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

Re: Float conversion

[Stephen Leake]

Georg Bauhaus <rm.dash-bauhaus@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

Re: Float conversion

[Robert A Duff]

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

Re: Float conversion

[Dmitry A. Kazakov]

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

Re: Float conversion

[Georg Bauhaus]

On 04.08.10 09:27, Stephen Leake wrote:
> Georg Bauhaus <rm.dash-bauhaus@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.

Suppose the code has, for a reason, the conditional

  if A = A then
  else
  end if;

That one can be important, J.-P. Rosen recently explained why,
talking about NaN. Is this test usually present?

Then, as Dmitry said, comparing Inf needs special care.  The meaning
of predefined "=" in some test case, for some floating point type,
can depend not just on platform, but also on platform state.
Practically, GNAT has, or used to have a state switching subprogram
that would turn on 80 bit FPT when running on Windows NT, IIRC.
Can a test make sure that results of "=" or even of "<" will be
unaffected by state switches in the processor?

What if significant epsilons change as computed results grow or shrink?

Additionally, can one write a test for ARM Something and hope
it gives the same result on a PC workstation for the
"same" program?


Georg

Re: Float conversion

[Phil Clayton]

On Aug 3, 11:38 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> 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".)

Yes.  Using a mathematical model where floating point values are
viewed as mathematical real numbers (i.e. having infinite precision)
and where operators have their standard mathematical meaning is an
approximation.  Reasoning with such a model of programs will detect a
useful and wide class of error but won't correctly predict the
behaviour of programs in absolutely every case.  It is easy to produce
examples that demonstrate this involving floating point equality and
values that cannot be represented exactly.

Phil

Re: Float conversion

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> (some things are stateful. A pipelined CPU pipeline definitely is. We
> used to ignore that, can we for "exhaustive" testing?)

If we can't we are all doomed.

Re: Float conversion

[Dmitry A. Kazakov]

On Wed, 04 Aug 2010 20:36:28 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> (some things are stateful. A pipelined CPU pipeline definitely is. We
>> used to ignore that, can we for "exhaustive" testing?)
> 
> If we can't we are all doomed.

That reminds me the old programmer's saying: never test for the bugs you
cannot fix.

(:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Float conversion

[Georg Bauhaus]

On 8/4/10 9:36 PM, Simon Wright wrote:
> "Dmitry A. Kazakov"<mailbox@dmitry-kazakov.de>  writes:
>
>> (some things are stateful. A pipelined CPU pipeline definitely is. We
>> used to ignore that, can we for "exhaustive" testing?)
>
> If we can't we are all doomed.

FPT programs are a little more complex to test in full anyway,
so exhaustion is relative  :-)

The subject seems to have been on the radar since the beginning:
http://archive.adaic.com/standards/83rat/html/ratl-05-03.html#5.3.1

With notes on "=" and "/=" and whether to provide these
operation at all with Ada floating point types.

Re: Float conversion

[Phil Clayton]

On Aug 4, 8:26 am, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> >> > 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?

Well, in practice, you would hope that if someone knew a specification
was wrong/incomplete that they wouldn't go ahead and implement it!

What if a specification is clear but - not obviously - contains
undesired features?  It can be argued that a convincing verification
is valuable regardless of the specification quality because, when
something goes wrong, you know that it is less likely to be an
implementation issue and more likely to be a specification issue.  So
it helps isolate issues.  In practice, any sane person would review
the specification first to reduce the likelihood of change and
subsequent process iteration.

So there are two separate issue here:
1. Is the specification capturing what is wanted (`validation')
2. Does the program implement the specification (`verification')

I was only considering 2 in this thread and trying to avoid the other
minefield that is 1!

Phil

Re: Float conversion

[Stephen Leake]

Robert A Duff <bobduff@shell01.TheWorld.com> writes:

> 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.

Yes, that's true.

> You seem to be using some sort of coverage metric, not exhaustive
> testing.

Yes.

>> 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!)

I was talking about my rewrite, which got rid of the 'and' operators to
make things clearer.

> And why not A=B-epsilon?

That's one appropriate test case for A < B, along with A = B - 1.0.

> By the way, putting:
>
>     pragma Assert (C < B and C < A);
>
> after "else" might have made the bug clearer.  Or might not.

That's a good idea.

>> 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.

That's what I meant; the verification process is meaningless without a
specification. 

-- 
-- Stephe

Re: Float conversion

[Shark8]

> 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!)

This could be written better as:


Function Min( A, B, C : SOME_TYPE ) is
begin
If A < B AND A < C then
   return A;                -- We know A is the smallest valued var
here...
elsif B < C then            -- and in the ELSE case we know that it is
not the smallest value.
                            -- If A is equal to C or B then returning
that value is equivalent to returning A's value.
   return B;
else                        -- We know here that C is the low-valued
parameter.
   return C;
end Min;

You could also add the Pragma 'inline' if you wanted.

Re: Float conversion

[Georg Bauhaus]

On 8/7/10 7:54 AM, Shark8 wrote:

> Function Min( A, B, C : SOME_TYPE ) is
> begin
> If A<  B AND A<  C then
>     return A;                -- We know A is the smallest valued var
> here...
> elsif B<  C then            -- and in the ELSE case we know that it is
> not the smallest value.
>                              -- If A is equal to C or B then returning
> that value is equivalent to returning A's value.
>     return B;

Generalizing, when Min returns not the values but identities,
will the equivalence of A and B work when stable sorting is needed?

Another question, are there algorithms that rely on
the representation of A, B, and C so that equivalence
doesn't establish equality?


Georg

Re: Float conversion

[Shark8]

On Aug 7, 2:56 am, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
wrote:
> On 8/7/10 7:54 AM, Shark8 wrote:
>
> > Function Min( A, B, C : SOME_TYPE ) is
> > begin
> > If A<  B AND A<  C then
> >     return A;                -- We know A is the smallest valued var
> > here...
> > elsif B<  C then            -- and in the ELSE case we know that it is
> > not the smallest value.
> >                              -- If A is equal to C or B then returning
> > that value is equivalent to returning A's value.
> >     return B;
>
> Generalizing, when Min returns not the values but identities,
> will the equivalence of A and B work when stable sorting is needed?
>
> Another question, are there algorithms that rely on
> the representation of A, B, and C so that equivalence
> doesn't establish equality?
>
> Georg

Good questions.
In regard to the stability, I'm under the impression that is a
property of the algorithm rather than the comparative-operation.
{For example Shell sort is NOT a "stable" sot, but it uses the same
operator that merge sort uses; merge sort *is* stable.}

For the equivalence/equality question I think it's a matter of the
data-type rather than the algorithm that determines it. For example we
could define a Set Type with the operation "<" returning true if Left
is a proper/strict subset of Right (that is to say fully contained by
the superset and NOT equal to it). Now, given a set [Red, Blue, Green,
Purple, Yellow, Gray] both [Red,Green,Blue] & [Red, Yellow, Blue] are
subsets thereof and return true for "<". However, neither of the
subsets are equal or subsets of one another; so we cannot use "<"
alone to determine how to 'sort' this group of sets.