From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,9b4538cfeb0c3576
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail
From: Stephen Leake <stephen_leake@stephe-leake.org>
Newsgroups: comp.lang.ada
Subject: Re: Float conversion
References: 
 <9e669a3b-1013-4bd1-b372-5f7dfa46d083@f42g2000yqn.googlegroups.com>
 	<1q5zc0ais535h$.1jqwfxhj9cflc$.dlg@40tude.net>
 	<4c519968$0$6893$9b4e6d93@newsspool2.arcor-online.net>
 	<1d1txn4x3r5xn.1trm4gx9n87gm$.dlg@40tude.net>
 	<cb7a898b-fe3b-424e-adfa-9dcc22ea570c@l20g2000yqm.googlegroups.com>
 	<1jo4xj7cntwy1$.1ntf9smcka8vf$.dlg@40tude.net>
 	<1d617940-d138-4b8c-a321-ed23b47431b8@x21g2000yqa.googlegroups.com>
 	<1naf3ekl5k916$.f7ugc92galdz$.dlg@40tude.net>
 	<d981aeab-67e9-4fde-a96c-ec6a2a403703@c10g2000yqi.googlegroups.com>
Date: Sat, 31 Jul 2010 11:12:34 -0400
Message-ID: <82y6cru1lp.fsf@stephe-leake.org>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (windows-nt)
Cancel-Lock: sha1:BAGFQIwc1GGQj4wl4sKysxueu7Y=
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Complaints-To: abuse@flashnewsgroups.com
Organization: FlashNewsgroups.com
X-Trace: e9b124c543d60e029e66110357
Xref: g2news1.google.com comp.lang.ada:12753
Date: 2010-07-31T11:12:34-04:00
List-Id: <comp.lang.ada>

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