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,FREEMAIL_FROM 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.96.231 with SMTP id dv7mr8386018wib.6.1356839640702; Sat, 29 Dec 2012 19:54:00 -0800 (PST) Path: l12ni269292wiv.1!nntp.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.81.MISMATCH!newsfeed.xs4all.nl!newsfeed2.news.xs4all.nl!xs4all!newspeer1.nac.net!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nrc-news.nrc.ca!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Mon, 24 Dec 2012 13:45:54 -0600 Date: Mon, 24 Dec 2012 14:45:53 -0500 From: "Peter C. Chapin" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/17.0 Thunderbird/17.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Exception contracts for Ada? 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> In-Reply-To: Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-s1SmEshnZCbpwdYV5hLCNzAvnY+AWIuiVLIOGEpxlTK6FWnCqwzEdglu97lMlpLjoAM/Fsfi/+e+a2e!OVe0wVXxCPw/3f3fxz5cV4DRUzc7Va06tu55eN/HG5Q62lJDJYr5ojJ/22RDZdM= X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 6049 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-12-24T14:45:53-05:00 List-Id: I know there be dragons down this road, but I will comment on a few of your points. First, I want to emphasize that I'm not necessarily disagreeing with you... just elaborating on some ideas. On 12/24/2012 11:34 AM, Dmitry A. Kazakov wrote: >> + Should exception contracts be enforced statically or dynamically? > > Statically. Contracts cannot be enforced dynamically, it is rubbish. I tend to agree that exception contracts should be enforced statically or else you end up with the mess C++ got itself into with its exception specifications. The problem of what to do at runtime if the contract is violated seems like a show-stopper for dynamic enforcement. >> + 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. >> + 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. 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. >> + 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? 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. >> + Should exception contracts be a part of a subprogram's type? > > There is no subprogram types in Ada so far. If I call a subprogram indirectly via an access value, what do I know statically about its exception contract? How can I statically check that the exception contracts are being honored? 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. > Do you mean the case when P calls to Q which is allowed to propagate E > while P promises not to propagate E? In that case if analysis shows that P > never propagates E, no special handler is required. 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." 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. Peter