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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.196.232 with SMTP id ip8mr8113069pbc.6.1341452728894; Wed, 04 Jul 2012 18:45:28 -0700 (PDT) MIME-Version: 1.0 Path: l9ni10938pbj.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!fdn.fr!gegeweb.org!news.ecp.fr!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Wed, 4 Jul 2012 20:45:20 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net> <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net> <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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341452726 32302 69.95.181.76 (5 Jul 2012 01:45:26 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 5 Jul 2012 01:45:26 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-07-04T20:45:20-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net... > On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net... >>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature >>> wrote: >> ... >>> They are contracts when checked statically and implementations when >>> checked dynamically. >> >> No, they're always contracts. They certainly aren't "implementation", >> because they do *not* belong to the subprogram; they're checked *before* >> the >> subprogram is called. > > Checked by whom? By the caller, not the called body. > How does this make any difference to the caller or to the > program as a whole? Is there a way to determine whether an exception was > raised in the body or "before" the body? Sure: you can handle an exception raised in the body in the body itself; you cannot handle an exception raised by the call in the body. > Maybe there is some special > before-the-body-exceptions, propagated in some special manner? It just > does > not make sense. It's been that way in Ada since at least Ada 80 -- exceptions raised by the call cannot be handled in the body, exceptions raised in the body can be handled in the body. Amazing to find out that the model "does not make sense" after 30+ years. ;-) It has never been the case that constraint failures are part of the effect of the subprogram; they're part of the effect of the call (and thus belong to the caller, not the callee). > The contract should refer to all effect of calling the program. It does. The call itself is not part of the effect of "calling the subprogram". >> Besides, I don't understand why it is such a disaster to have >> precondition >> contracts be dynamically evaluated in some cases, while it is OK to have >> a >> postcondition be dynamically evaluated in some cases -- it too is a >> contract >> (one that is evaluated *after* the subprogram finishes). > > It is *not* OK to evaluate precondition of a program by the program > itself. Well, then the precondition would never be evaluated at all, because there is nothing else. In my world, at least, Ada is the only programming language -- we even used Ada as the language of the command line of our debugger. The notion of using some other language and some other program to describe program semantics is a non-starter. Randy.