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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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.91.114 with SMTP id cd18mr9914377wib.2.1356837411617; Sat, 29 Dec 2012 19:16:51 -0800 (PST) Path: i11ni337243wiw.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.103.MISMATCH!feeder3.cambriumusenet.nl!feed.tweaknews.nl!94.232.116.13.MISMATCH!feed.xsnews.nl!border-3.ams.xsnews.nl!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Exception contracts for Ada? Date: Tue, 25 Dec 2012 12:09:12 +0100 Organization: cbb software GmbH 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: 6/SyjDFvQ5V7ZR2+GYgbDQ.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-12-25T12:09:12+01:00 List-Id: On Mon, 24 Dec 2012 14:45:53 -0500, Peter C. Chapin wrote: > 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: > >>> + 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. It must be so, even if the language were developed from scratch. The problem is that exception checks are evidently undecidable. It means that you must have a grey zone for the things you cannot prove either true or false. Of course some legacy stuff could be much better if contracted. E.g. a promise not to raise anything in Finalize/Initialize, but that would indeed break legacy code. >>> + 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. But a program is not required to have a specific exception contract. The language should not enforce that. The default contract is: I can raise anything. >>> + 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? Yes > Will it be necessary to add syntax so that generic > formal parameters can have their exception contracts declared? Possibly, e.g. formal exception, formal set of exceptions as generic parameters. > 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. Sure, any [object] language aspect may have a generic counterpart [in the meta language]. That should rather bother people pushing for more generics. To me it makes little sense to invest any efforts into further developing of obviously lousy concept. >>> + 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? This looks simple. When you declare an access to subprogram type, that declaration will have an exception contract (possibly empty). E.g. type P is access procedure ... with exceptions => E1; E1 is an exception contract. Now let you declare procedure F ... with exceptions => E2; Then F'Access matches P if parameters do and E2 implies E1. Since contracts are statically checked, you can check that at compile time. [ A very useful thing for bindings, preventing passing Ada callbacks raising exceptions to C libraries ] > I do know that, in GNAT at least, preconditions can't be declared for > access to subprogram types. For dynamic checks there is little difference anyway. I suppose >> 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. Yes, that is the most difficult part of it, specification what is required to be provable about exceptions = anything else is mandated to be considered non-provable, even if you or compiler knows otherwise. Although exception checks could be very, very conservative. I don't think anything more sophisticated than what Ada mandates, for example, for presence of return statements in the function body is required. Static analysis could simply look after all calls the body does and merge their contracts [so for any block having handlers]. One could refine this a bit towards if- and case-statements with static expressions, but that is not really needed, IMO. > It seems to me that's a case where the standard is actively interfering > with the capabilities of an advanced compiler. The language, especially its type system, is full of such things. When you do type T is new Integer; then T is treated as another type, though you and the compiler know them same. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de