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,7d3cb5920e882220 X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!feeder.erje.net!nuzba.szn.dk!news.jacob-sparre.dk!pnx.dk!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Contracted exceptions for Ada Date: Tue, 11 Dec 2007 18:26:06 -0600 Organization: Jacob's private Usenet server Message-ID: References: <5947aa62-2547-4fbb-bc46-1111b4a0dcc9@x69g2000hsx.googlegroups.com> <7m9wkymyi5h7.1235e72is9mp9.dlg@40tude.net> <185k0c8e598ko.16o5j2iv35zpn$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: jacob-sparre.dk 1197572263 4072 69.95.181.76 (13 Dec 2007 18:57:43 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 13 Dec 2007 18:57:43 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2800.1914 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1914 Xref: g2news1.google.com comp.lang.ada:18926 Date: 2007-12-11T18:26:06-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:185k0c8e598ko.16o5j2iv35zpn$.dlg@40tude.net... > On Mon, 10 Dec 2007 19:53:27 -0600, Randy Brukardt wrote: ... > > That's not going to be useful, since virtually any code that you can write > > *might* raise Constraint_Error, > > Why is it a problem? Because every contract would have to include Constraint_Error, and that would add a huge amount of verbiage to programs for no benefit. Or you have to exclude it from the contract like Java does, which would be worse. > > and a lot of code *could* raise > > Program_Error, and everything *could* raise Storage_Error. There is no way > > to write a contract that doesn't contain those exceptions. > > Program_Error is not my concern. Storage_Error can be fixed as I described > earlier. Program_Error *is* your concern. There is no way that a compiler could prove that it would not be raised from a lot of code; as such it would have to be included in the contract even though it isn't interesting to anyone (presuming again static contract checking and no "unchecked" exceptions). And your solution for Storage_Error adds a large number of new rules to the language, and is unlikely to make it possible to eliminate the exception. For instance, other tasks can allocate memory for the heap, so the only possible way to tell if you are out of heap memory is to catch the exception -- anything else is a race. And Janus/Ada at least uses heap memory to allocate virtually everything not statically sized: pretty much anything other than an elementary object or "null;" can raise Storage_Error in Janus/Ada. Besides, you say you don't want to add preconditions and the like, and then you do exactly that to handle Storage_Error. Can't have it both ways... > And for all, what I meant under exception contracts was not about making a > program exception-free. It was about specifying which exception can > propagate and which cannot. Right, but the predefined exceptions can always propagate. The only way to prove that they don't is to do extensive static analysis, and that isn't happening in the language. > >>> Another one is what to do if a contract is violated. The obvious answer of > >>> raising Program_Error doesn't do anything other than lose information about > >>> an exception, so that isn't very satisfying. > >> > >> Yes, in my view exception contracts have to be static. (It makes no sense > >> to have run-time exception contracts. As well as any other contracts, there > >> is no any authority body to judge contract violations at run-time.) > > > > OK, but that isn't going to happen in Ada. What you are looking for is a > > static analysis tool, like SPARK. That's especially true as you'll need > > static preconditions to have any hope of eliminating the Constraint_Errors > > (subtypes aren't powerful enough). > > This is a separate issue. You seem to imply that the exception contracts > shall specify *when* an exception is raised or not. That is a much harder > problem and it indeed would require pre- and postconditions and cannot be > done in general case. What I am talking about is a much weaker framework > which only proves whether an exception cannot propagate. We do not need > pre-/postconditions for that. > > A comparable case is exact real vs. interval arithmetic. We don't need > exact exception propagation analysis, we do a conservative *estimation* of. Right, but a the only possible conservative estimate is that all code can propagate Program_Error, Constraint_Error, and Storage_Error. Even exception when others => null; can raise Storage_Error and Program_Error (from finalization). And if you replace "null" with a subprogram call, you will probably introduce Constraint_Error. Unless you do quite a bit of static analysis, you can't prove *anything* useful about what exceptions can propagate. Java solves this by excluding the predefined exceptions, but all that does is makes the contracts useless -- you don't really know what might propagate. I hardly ever have problems with user-defined exceptions like Windows_Error or Not_Valid_Error (from Claw, as an example) propagating: the "comment" contracts make it pretty clear what can happen, and expected errors are quickly handled. Without some sort of static analysis required, all access dereferences *can* raise Constraint_Error, all integer assignments can raise Constraint_Error, and so on. Since we want all Ada compilers to work the same (so code is portable), you would have to define what exact rules you are allowed to use for determining whether an exception is raised, and which ones you are not. That is a significant effort, and is going to be hard for some compilers to implement -- moreover, compilers that know more would have to be prohibited from using it. None of that seems good. Randy.