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 Path: g2news1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!bloom-beacon.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: Float conversion Date: Wed, 04 Aug 2010 08:52:40 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: 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> <1jo4xj7cntwy1$.1ntf9smcka8vf$.dlg@40tude.net> <1d617940-d138-4b8c-a321-ed23b47431b8@x21g2000yqa.googlegroups.com> <1naf3ekl5k916$.f7ugc92galdz$.dlg@40tude.net> <82y6cru1lp.fsf@stephe-leake.org> <77ee8883-ab9f-42c7-94d5-3d85cdc19693@i28g2000yqa.googlegroups.com> <82pqxyu9bw.fsf@stephe-leake.org> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Trace: pcls4.std.com 1280926345 32567 192.74.137.71 (4 Aug 2010 12:52:25 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Wed, 4 Aug 2010 12:52:25 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:9Z1uXbYcTUGBw74fi4TQmwK/eb4= Xref: g2news1.google.com comp.lang.ada:12850 Date: 2010-08-04T08:52:40-04:00 List-Id: Stephen Leake writes: > Phil Clayton writes: > >> On Jul 31, 4:12�pm, Stephen Leake >> 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