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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,640b65cbfbab7216 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!z24g2000prf.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Mon, 14 Apr 2008 18:35:05 -0700 (PDT) Organization: http://groups.google.com Message-ID: <8862aecc-c70d-46cc-a140-f26d9b0acfb4@z24g2000prf.googlegroups.com> References: <47F26C46.3010607@obry.net> <44d88b93-6a90-4c18-8785-2164934ba700@a9g2000prl.googlegroups.com> <47F652F7.9050502@obry.net> <47f7028d$1_6@news.bluewin.ch> <47F749CB.30806@obry.net> <728033b9-52c1-4951-ba22-5067467dad50@b5g2000pri.googlegroups.com> <90d313e2-115b-4998-ad2d-3d0c4d84f841@q24g2000prf.googlegroups.com> <48039eb1$0$629$9b4e6d93@newsspool1.arcor-online.net> NNTP-Posting-Host: 166.70.57.218 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1208223306 9145 127.0.0.1 (15 Apr 2008 01:35:06 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 15 Apr 2008 01:35:06 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: z24g2000prf.googlegroups.com; posting-host=166.70.57.218; posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.13) Gecko/20080311 Firefox/2.0.0.13,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:20947 Date: 2008-04-14T18:35:05-07:00 List-Id: On Apr 14, 12:13 pm, Georg Bauhaus wrote: > It might be worth noting that this kind of "correctness" > specifically precludes factors that are essential to typical > Ada programming: for a program to solve a problem correctly, > use of time and storage must stay within specified bounds, too. > > Is there a definition of "correctness" that includes more than > the necessary, static, computer agnostic precondition > of "left side of equation equals right side of equation" no > matter when and how? Yes. To me, the quickest way of getting at the essence of such conditions is to start trying to write them down. You need symbols for that. You need a function symbol for, say, the time something takes and another for the space something takes. You need units of time and units of space for the results. You need literal expressions for durations of time and amounts of space to write down bounds. All these are analytical symbols that need not be part of the language they are analyzing. The traditional method of correctness uses only the symbols of a programming language combined with those of predicate calculus. Simply from lack of expressibility, this traditional method cannot directly address issues of time and space. You need to obtain those symbols from somewhere, and this pretty much means constructing an execution model that provides a place to root those symbols. Execution models, however, are properties of the target processor and execution environment, and thus outside of and, really, independent of the abstractions of high-level languages. So, to ground this in Ada, should there be a Ada-wide execution model? Probably not. Might there be someday a way of expressing an execution model in Ada? I would hope so. One of the consequences of this is that, in general, you can't prove performance predicates about a program by itself, but only together with an execution model. Admittedly most execution models are similar, but it would be a error of categories to assert a universal one. (I don't mean to say that a canonical one might not be useful.) There's a whole area of practical experience to gather about the similarities of such proof prior to standardization, and I wouldn't rush in quickly. Finally, in order for this to work, you have to be able to connect execution of the high-level program with execution of a program of equivalent effect in the execution model. This is where that Hoare paper that I mentioned a while back, "Proof of correctness of data representations" comes in. It describes exactly how this works. Eric