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.180.74.79 with SMTP id r15mr9895653wiv.4.1356837414398; Sat, 29 Dec 2012 19:16:54 -0800 (PST) MIME-Version: 1.0 Path: i11ni337233wiw.0!nntp.google.com!feeder3.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.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!newsfeed.straub-nv.de!reality.xs3.de!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? Date: Wed, 26 Dec 2012 20:38:08 -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 1356575892 15779 69.95.181.76 (27 Dec 2012 02:38:12 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 27 Dec 2012 02:38:12 +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:38:08-06:00 List-Id: "Peter C. Chapin" wrote in message news:XYadnZrAFoJvLUXN4p2dnAA@giganews.com... ... >>> + What about backward compatibility with the existing code base? >> >> No problem at all. Empty (missing) contract = any exception may >> propagate. >> Everything would be 100% compatible. > > But is that what we would want? I'm not sure. There is no other possibility. One could imagine a restriction that required a contract on every subprogram. But as we found out with "overriding", that way lies dragons. My personal opinion is that what Java got wrong was the default. "anything can be raised" is much friendlier than making people stick junk handlers in everywhere or change their contracts repeatedly. Some interfaces have to be designed in stone (like those for Claw, Ada.Containers, etc.), but most don't need that level of contracting. >>> + 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? >> >> There is no such distinction. > > Java does not require exception specifications for certain classes of > exceptions such as for dereferencing null pointers and similar low level > (language support) things. If it did then virtually every method would > need to be decorated with an exception specification. Right; here again, this is what Java got wrong. By making the default "no exceptions", the contracts got immediately out of hand. And they then fixed that by excepting some exceptions from the contracts, making the contracts like swiss cheese. They never worked their way out of the morass -- proving again that two mistakes don't make something usable. :-) > In Ada there are, for example, so many ways Constraint_Error can be raised > that requiring it to be contracted by every subprogram seems... wrong > somehow. No, the preconditions/predicates should prevent it from being raised, and the compiler should be able to prove that. So it doesn't need to be in most of the contracts. (If a Claw subprogram raises Constraint_Error, it's a bug!) To me this is a big benefit of these contracts: you can *declare* exception absence, and the compiler will either prove it or fail to the code -- no restrictive and separate tool like Spark needed for that. (Which brings that particular benefit of Spark to everyone.) >>> + How should exception contracts interact with generic code? >> >> As any other language thing does. Generic code has "generic contracts" >> which become normal contracts after instantiation. > > The interesting part is not the contracts on the generic code itself but > rather on the entities used by the generic code. Are exception contracts > on generic code to be checked when the generic code is compiled or at > instantiation time? Will it be necessary to add syntax so that generic > formal parameters can have their exception contracts declared? Yes, of course. Otherwise, they're "raise any". But perhaps we won't do this any more than we do it for preconditions. (As far as I can tell, this prevents any proofs of a generic unit before instantiation, and makes the proofs "fragile" as a different instance might fail. This is not Ada to me...) > I suppose there are similar questions surrounding the interaction of pre- > and postconditions and generic code. I'm not sufficiently up on Ada 2012 > yet to know how those issues are currently handled but I'm guessing that, > because they are dynamic checks, the compiler doesn't worry about them. Right, and I'm pretty sure this is wrong (but too hard to fix, as it would require "matching" of arbitrary expressions - conformance is close but it doesn't work because the types would be different). ... > I do know that, in GNAT at least, preconditions can't be declared for > access to subprogram types. Instead the preconditions are checked as the > pointed-to subprogram is entered. I'm not sure if that's ideal but in any > case it seems to make some sense for dynamically checked preconditions. > For statically checked exception contracts, though, it seems like > something more is needed. More is needed for preconditions, too, unless you never want to prove anything and make only dynamic checks. My guess is that access-to-subprogram is inherently unsafe from a proof perspective, and nothing is going to fix that. So there is no point in adding lipstick to a pig -- especially if the attempt to do so would make the entire proposal too complex (a real problem in Ada language proposals). ... > Yes that's basically what I mean. What you are suggesting sounds like it > would require mandating a certain level of static analysis in compilers. > Otherwise how could one write a portable program? I could imagine a very > advanced compiler saying, "I can see that Q will never raise E in this > situation but at the level of analysis mandated by the standard it would > not be possible to tell that. Thus I'm going to require you to put a > contract on P anyway declaring that P might raise E (even though you and I > both know it won't) for portability to lesser compilers who will require > it." I think that the "solution" is that the "proof" is implementation-defined for language-defined checks. Which means that a program with "static" exception contracts might not be portable to a "dumb" compiler. That's annoying, but I think any alternative is going to turn out much worse (but I'm happy if someone wants to try to prove me wrong). Certainly, trying to define checks that have to be optimized away is going to be madness, and not using the knowledge that the compiler has is also madness. After all, "canonical semantics" says that A : Integer := 10; might raise Constraint_Error, but I'd be amazed if there is any compiler that generates a check in this case. I think only "implementation-defined" is likely to work. This is clearly the weak point of my proposal (and any useful exception contracts, IMHO). > It seems to me that's a case where the standard is actively interfering > with the capabilities of an advanced compiler. > > On the other hand the idea of mandating some level of static analysis may > be an idea who's time has come. I'm thinking again about pre- and > postconditions. Specifying it would be difficult, I imagine. I don't think it's time will ever come, simply because trying to do so will take up a lot of time and effort. I really have no idea how to describe that formally that could be understood (look at 11.6 to see how well that has been explained in past standards :-). Randy.