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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.223.40 with SMTP id qr8mr20011681pbc.0.1340799578740; Wed, 27 Jun 2012 05:19:38 -0700 (PDT) Path: l9ni25678pbj.0!nntp.google.com!news2.google.com!goblin3!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Wed, 27 Jun 2012 14:19:38 +0200 Organization: cbb software GmbH Message-ID: <2klq69d4qqsp$.veefi8i6jnwa.dlg@40tude.net> References: <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> <4feae0d1$0$6568$9b4e6d93@newsspool3.arcor-online.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-06-27T14:19:38+02:00 List-Id: On Wed, 27 Jun 2012 12:30:41 +0200, Georg Bauhaus wrote: > 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? That the code is in disagreement with your objective. > 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. This is wrong on multiple accounts: 1. It cannot be shown: if Pre (HALT (p)) then ... else ... end if; 2. For any program there exist an infinite set of contracts satisfied by; 3. It is irrelevant to whether both pieces are equivalent. If they are, one can be replaced by another. DO IT, where is the check? If they cannot be swapped, they are not equivalent. (Your previous position was more consistent. The point can only be made by getting rid of logic first.) >> They evidently do not have same effect. Prove that they do! > > A and B have *essentially* the same effect once the program > is correct. I don't know what "essentially same effect" is, but whatever formal definition of essential you took you would have to prove that two programs are equivalent according to the definition. That will require proving that the exception is not propagated or else handled to an "essentially" same result. Good luck with that. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de