From: Henrique on
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...(a)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...(a)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 -

From: Dmitry A. Kazakov on
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
From: Stephen Leake on
Phil Clayton <phil.clayton(a)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
From: Phil Clayton on
On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)stephe-leake.org>
wrote:
> Phil Clayton <phil.clay...(a)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
From: Shark8 on
On Aug 2, 7:07 pm, Phil Clayton <phil.clay...(a)lineone.net> wrote:
> On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)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.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5 6 7
Prev: What is your preferred VCS?
Next: GPS 2010 for AVR