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.227.67 with SMTP id ry3mr1731431pbc.8.1341293317947; Mon, 02 Jul 2012 22:28:37 -0700 (PDT) MIME-Version: 1.0 Path: l9ni10736pbj.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!newsfeed.utanet.at!newsfeed.tele2net.at!newsfeed.straub-nv.de!nuzba.szn.dk!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: Tue, 3 Jul 2012 00:28:31 -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 1341293316 20004 69.95.181.76 (3 Jul 2012 05:28:36 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 3 Jul 2012 05:28:36 +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-03T00:28:31-05:00 List-Id: "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. (The check, if any, belongs to caller, not the callee.) 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). In any case, you want to prevent the any mechanism for specifying these things in code rather than in comments are currently. It should never be necessary for anyone to look into the body ("implementation") of a routine to see the contract (static or dynamic); tools that have to see within bodies (that is, only operate on all of the source) are close to useless (since they can only be used at the end of the development cycle when fixing bugs is at its most expensive). ... >> So you just add "can raise Storage_Error" to any contract? (Maybe >> implicitly.) > > Contracts will be inheritable. I don't know how it goes with aspects, > never > understood what they are good for, but true contracts are inherited while > possibly weakening pre- and strengthening post-conditions (LSP). Yes, of course. Class-wide preconditions are inherited (potentially with weakening, although that's almost never useful), as are class-wide postconditions (with strengthening). (Don't use specific preconditions and postconditions if you care about inheritance.) > Another necessary contract mechanism is composition. That is when you pass > a downward closure to an operation, that could say: I raise what the > argument does. Note that this will require proper procedural types to have > interfaces to carry the contract with. E.g. you would be able to limit the > closure operation to what it is allowed to raise. I agree with the need for composition; we had that in the never-finished "global in/out" contracts. But that doesn't require "procedural types" per-se; it can be done quite easily with the existing facilities. (Whether the result really would be any good, I can't say, but I'm pretty sure that the existence of "procedural types" would make no difference in how useful is is.) ... > The real problem lies elsewhere. Prover to tell program legality is thin > ice. Depending on the technique used the same program could be legal (good > prover) or illegal (poor prover). I don't know how to address this, though > nobody cares anyway... I think some of us care, the problem is assuming that the prover can prove everything important (that will never, ever happen). For me, the biggest impediment is coming up with rules that would allow proving what they can without (a) requiring too much of all compilers and (b) bounding what an implementation can do. There's clearly a portability problem here -- it's quite possible that that problem will prevent ever implementing exception contracts in the Ada language (as opposed to specific implementations). Randy.