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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!news3.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!ecngs!feeder2.ecngs.de!news.netcologne.de!ramfeed1.netcologne.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Float conversion Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH 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> Date: Wed, 4 Aug 2010 16:32:46 +0200 Message-ID: <1uuvx10ynvzyw.1g2rh2mpso9j.dlg@40tude.net> NNTP-Posting-Date: 04 Aug 2010 16:32:45 CEST NNTP-Posting-Host: 629c86a7.newsspool2.arcor-online.net X-Trace: DXC=eMd`fbQKjVLFJ3]dH>I?oEA9EHlD;3YcB4Fo<]lROoRA8kF On Wed, 04 Aug 2010 08:52:40 -0400, Robert A Duff wrote: > Stephen Leake 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