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,UTF8 Received: by 10.68.241.162 with SMTP id wj2mr9526401pbc.2.1341490025231; Thu, 05 Jul 2012 05:07:05 -0700 (PDT) Path: l9ni10938pbj.0!nntp.google.com!news1.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!195.62.100.242.MISMATCH!newsfeed.kamp.net!newsfeed.kamp.net!newsfeed.straub-nv.de!uucp.gnuu.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 05 Jul 2012 14:07:02 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:13.0) Gecko/20120614 Thunderbird/13.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net> <13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net> In-Reply-To: <13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net> Message-ID: <4ff58367$0$6643$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 05 Jul 2012 14:07:03 CEST NNTP-Posting-Host: ddb537ec.newsspool2.arcor-online.net X-Trace: DXC=i9;5ejLh>_cHTX3jm4W=enMRk=Yf X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Date: 2012-07-05T14:07:03+02:00 List-Id: On 05.07.12 10:48, Dmitry A. Kazakov wrote: > On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: >> ... >>>> Legality has nothing to do with preconditions or postconditions. >>> >>> => It is OK to violate a "contract" defined by these. Here you are. >> >> No, it's not OK; that is the crux of our disagreement. You seem to think >> that the only kind of "contract" is some sort of static thing. > > Exactly. Because the contract exists *before* any programs implementing it > and after them. The contract exists even when there is no such program. OK > Therefore it cannot depend on the program state. The "therefore" does not follow, because "it" makes too far reaching assumptions, from which, I think, no one suggests your logic does not follow. "It", for a start, once it materializes in this or that form. Contract checking built into a program is rather a design tool than some oracular inference engine. Correctness need not be assumed at this stage. If the checks are severely flawed bacause some programmer inserts viral side effects in checked expressions, or just wishes to start from the proof of the absence of 666 consecutive digits of e in π on the way, then so be it. He or she is violating the goals of designing with the help of assertions. The goal is *not* unrolling proven assumptions into source text, but arriving at proven systems. So that turning off assertion checking can be considered safe. Safe because checking will not affect the desired effect of the program in any way that is covered by the contract-as-agreed as being essential. So IMHO Pre/Post/Inv are really improvements of pragma Assert. > Another way to understand this: a contract describes states of a program. That's not a contract. There are no parties. There is no obligation to make predicates true on either side. A program could define states, in the contract's space.