Re: Float conversion

[Stephen Leake <stephen_leake@stephe-leake.org>]

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