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!postnews.google.com!t2g2000yqe.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Float conversion Date: Thu, 5 Aug 2010 03:20:40 -0700 (PDT) Organization: http://groups.google.com 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: 89.242.151.47 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1281003640 7562 127.0.0.1 (5 Aug 2010 10:20:40 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 5 Aug 2010 10:20:40 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: t2g2000yqe.googlegroups.com; posting-host=89.242.151.47; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15) Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:12874 Date: 2010-08-05T03:20:40-07:00 List-Id: On Aug 4, 8:26=A0am, Stephen Leake wrote: > >> > Where does the original justification go wrong? =A0Well, when talkin= g > >> > about 'the smallest' there is an implicit assumption being made that > >> > it is unique. =A0The justification never considers the case when A o= r 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. =A0Any specification, > > formal or not, can be a load of rubbish! > > What are you verifying, if not a specification? > > If the specification is rubbish, what is the point of verifying it? Well, in practice, you would hope that if someone knew a specification was wrong/incomplete that they wouldn't go ahead and implement it! What if a specification is clear but - not obviously - contains undesired features? It can be argued that a convincing verification is valuable regardless of the specification quality because, when something goes wrong, you know that it is less likely to be an implementation issue and more likely to be a specification issue. So it helps isolate issues. In practice, any sane person would review the specification first to reduce the likelihood of change and subsequent process iteration. So there are two separate issue here: 1. Is the specification capturing what is wanted (`validation') 2. Does the program implement the specification (`verification') I was only considering 2 in this thread and trying to avoid the other minefield that is 1! Phil