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: a07f3367d7,6327f05d4989a68d X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.181.12.35 with SMTP id en3mr9738084wid.2.1356837414282; Sat, 29 Dec 2012 19:16:54 -0800 (PST) MIME-Version: 1.0 Path: i11ni337243wiw.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.131.MISMATCH!xlned.com!feeder3.xlned.com!news.astraweb.com!border6.a.newsrouter.astraweb.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!weretis.net!feeder1.news.weretis.net!feeder.erje.net!eu.feeder.erje.net!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: Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO Date: Wed, 26 Dec 2012 20:16:27 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net> <14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net> <1drh1q1ln2dfh$.a9hwlg01fjfy.dlg@40tude.net> <50d6365d$0$6577$9b4e6d93@newsspool3.arcor-online.net> <1pbg79bz92j3t$.sz41zduivjfp.dlg@40tude.net> <46idnVdMEr8J5EXN4p2dnAA@giganews.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1356574590 15116 69.95.181.76 (27 Dec 2012 02:16:30 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 27 Dec 2012 02:16:30 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-12-26T20:16:27-06:00 List-Id: "Peter C. Chapin" wrote in message news:46idnVdMEr8J5EXN4p2dnAA@giganews.com... ... > Exception contracts are a huge, HUGE topic and one that shouldn't be > treated too lightly. We've had this discussion within the ARG. It's pretty clear to me what the answers are (but others may not agree). See AI12-0017-1 for my take on this. (The ARG has not yet discussed this AI.) The problem in other languages is requiring them everywhere -- I'm pretty certain that will never work. They're critical for properly defining reusable code, but I'm dubious that they have much value in "top-level" code (the stuff that is created to use those reusable libraries). Good reusuable libraries are very hard work, and the more help the compiler can give the better... ... Consider: > + Should exception contracts be enforced statically or dynamically? Statically. Dynamic enforcement is a total can of worms with no real value. The real question is whether the enforcement can depend on implementation-properties (that is, if the implementation can optimize away a check, can that be used in enforcing the contract), or whether it has to remain portable. > + Should exception contracts be enforced at all or only produce warnings > or logs? That's worthless from an language perspective; pretty much the only value beyond the comments that we already use is static checking. Personally, I'm not interested in adding features to Ada that can't be used by an Ada compiler (but only be separate tools). > + What about backward compatibility with the existing code base? We don't > want to force people to decorate all code with exception contracts before > it will compile again with Ada 2020 (or whatever). Do we? Clearly, the default has to be "raises anything", we can't make everything incompatible. As best as we can tell, the root problem in C++ and Java is that the default is more restrictive. (Stupid coding policies probably don't help, either.) > + Should exception contracts distinguish between "impossible" exceptions > that shouldn't occur in a correct program (like Constraint_Error) and > "normal" exceptions that pertain to environmental problems such as invalid > input data? IMHO, no. The biggest value to these contracts is proving that language-defined exceptions don't occur (the compiler knows far more about this than any tool can figure out, as only it knows whether or not a check is generated for a particular operation in the code). The only exception that defies most such proofs is Storage_Error (and it can be eliminated in specialized circumstances). So I think everything should be specified. In order to cut down the size of such contracts, I've proposed allowing creating "sets of exceptions", so that only the single name of the set need be mentioned. > + How should exception contracts interact with generic code? I don't see any real problem here; a formal subprogram has to have an optional contract, and if it does, it has to "match". > + Should exception contracts be a part of a subprogram's type? Consider > access to subprogram values and their usage. Access-to-subprograms are probably going to always be "raises anything". This is very similar to the way preconditions work; one might expect that access-to-subprograms should allow preconditions and require some sort of matching, but that's just too complicated so it's purely dynamic. This will mean that access-to-subprograms won't be able to be called from inside of exception contracted subprograms. But the only effect of that will be to encourage avoiding access-to-subprogram completely (a very positive result, IMHO, you can't prove anything about a call to an access-to-subprogram in Ada 2012 and I doubt that will change). > + How should exception contracts interact with other static analysis > techniques? For example if a subprogram has a contract that says it might > raise exception E, but if static analysis can prove that a particular > usage will not actually raise E, does the programmer have to declare a > contract on the calling subprogram about E? One objection I've heard about > exception specifications in Java is that they require programmers to > either specify (or handle) exceptions that "clearly" can never actually > arise at that particular program point. See my answer to the first question. I strongly lean toward the implementation-defined static check (I'd be against adding the contracts at all if that isn't the case), but I'm pretty certain that is going to be a tough sell (it will harm portability, as a compiler that isn't as "smart" may not be able to tell that the exception isn't raised). The alternative of mandating what Ada compilers are required to be able to deduce is unlikely to work; it would be fiendishly complex and would add a great burden to at least some implementations. (Which would cause a lot of resistance, I think.) > Now that Ada has preconditions the last point is particularly acute. The > precondition on a procedure P might guarantee that a called subprogram > won't raise an exception that it might nevertheless declare in its > exception contract. That would be wrong; the exception contract should not cover things included in the precondition. And if the precondition is necessary to prevent an exception from being raised by the body, then the subprogram specification should be declared so that the precondition cannot be ignored. (That shouldn't prevent the compiler from eliminating it if it is redundant, just that it should never be unchecked.) > It would be really unpleasant if the programmer had to also add an > exception contract to P stating that it might raise an exception that the > programmer knows the precondition will prevent! As above, that's not how I envision these things working. (But please keep in mind, most of this is my feverish musing and it hasn't been vetted by others yet.) > This is just a sample of some of the issues involved in the subject. There > are those who have answers for all of these issues. That would be me, editor of the ARG and the Ada Standard. ;-) > That's great. But again I sincerely hope that if exception contracts are > ever seriously considered for Ada that the matter be given the deep > consideration it deserves. I hope you don't think that I just wrote this up based on absolutely nothing -- I've been thinking about how this would work since we started working on Claw...and I've taken input from many members of the ARG. (As well as discussions on these topics that the ARG had for Ada 2005, and a lengthy e-mail thread that we had specifically on the topic of what Java did wrong here). We have not yet had a formal discussion on this particular proposal, and I'm certain that it isn't 100% correct at this point (I must have forgotten something!). But it's rather insulting to have someone claim that it hasn't been given proper consideration before making a proposal (or to imply that the ARG would simply adopt something without thinking about it). Randy.