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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.190.104 with SMTP id gp8mr19745522pbc.4.1340793042778; Wed, 27 Jun 2012 03:30:42 -0700 (PDT) Path: l9ni25404pbj.0!nntp.google.com!news1.google.com!goblin3!goblin.stu.neva.ru!news.tu-darmstadt.de!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 27 Jun 2012 12:30:41 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:12.0) Gecko/20120428 Thunderbird/12.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net>

<4fe9bde5$0$6566$9b4e6d93@newsspool4.arcor-online.net> <4fe9e7c5$0$6567$9b4e6d93@newsspool4.arcor-online.net> <4feac313$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1et105d0sks1i.pcgog9ym17ym.dlg@40tude.net> In-Reply-To: <1et105d0sks1i.pcgog9ym17ym.dlg@40tude.net> Message-ID: <4feae0d1$0$6568$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 27 Jun 2012 12:30:41 CEST NNTP-Posting-Host: 1b8fe22f.newsspool3.arcor-online.net X-Trace: DXC=Rjih=UbljeH2jYf>V4L0gLMcF=Q^Z^V3H4Fo<]lROoRA8kF_5CCM><;OPCY\c7>ejVH_Yl1P7@ X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-06-27T12:30:41+02:00 List-Id: On 27.06.12 10:52, Dmitry A. Kazakov wrote: > On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote: > >> On 26.06.12 21:43, Dmitry A. Kazakov wrote: >> >>>> is supposed to >>>> implement something that essentially agrees with Pre/Post. >>> >>> Sure. Anything that follows "then" in any if-statement implements something >>> in agreement with the condition tested by the statement. That is the nature >>> of if-statements. >> >> That's not what agreement of with Pre/Post should mean, > > If that is not, change the code. Bugs not to be tolerated. What bug? I am defining what it means for a statement to, in essential effects, agree with what an explicitly stated Pre says, the latter being part of an ante factum contract. Consider A: if Pre (...) then A (X) := 1; else raise Assertion_Failure; end if; B: A (X) := 1; A and B can be shown to both be implementations of the behavior that some contract stipulates. Just like these implementations of a Procedure Add_2 (X : in out Integer) can be essentially the same X := X + 1; null; X := X + 1; X := X + 2; A compiler might produce code for these that, for example, is not efficient enough. If there is no efficiency constraint stated as part of the contract, the difference is unessential, and the two implementations are essentially the same, judging by the contract. > They evidently do not have same effect. Prove that they do! A and B have *essentially* the same effect once the program is correct. "Essential effects" is an important consideration when designing a program. With or without DbC, one choice can be just as good as another if they yield essentially the same effect. Unessential things do not count here. The bug hunting features of DbC do, as does the value it adds to documentation. We would not be using compilers or high level languages at all if there wasn't that notion of "essentially the same".