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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,deeb88b0e7eede4f X-Google-Attributes: gid103376,public From: bobduff@world.std.com (Robert A Duff) Subject: Re: Help with Exceptions! Date: 1996/05/15 Message-ID: #1/1 X-Deja-AN: 155034701 references: <4mmimq$s4r@hatathli.csulb.edu> <4nd7cm$fnp@watnews1.watson.ibm.com> organization: The World Public Access UNIX, Brookline, MA newsgroups: comp.lang.ada Date: 1996-05-15T00:00:00+00:00 List-Id: In article <4nd7cm$fnp@watnews1.watson.ibm.com>, Norman H. Cohen wrote: >A formal approach to a program with exception handlers is to establish a >postcondition for the block statement (or other frame) containing the >handlers. One then proves that > >(1) the postcondition is satisfied if the handled sequence of statements > completes normally; and > >(2) the postcondition is satisfied if the frame completes by invoking one > of the handlers. Quite reasonable. But Ada doesn't have any way to declare which exceptions are raised by which subprograms. I thought the earlier poster was saying that one should "know about" all the raise statements, which is what I was objecting to. Viewing the exceptions potentially raised by a subprogram as part of that subprogram's interface, would be much more reasonable, IMHO. But that's not simple -- consider a subprogram that takes an access-to-subprogram as a parameter. To reason precisely, you would sometimes like to say that the first subprogram raises whatever exceptions can be raised by its parameter (which is not known until run time). In any case, Ada doesn't have any way of saying these things, other than with comments. >A naive view is that proving (2) entails proving, for each statement in >the handled sequence of statements, that if that statement raises some >exception handled in the frame, then the execution of the handled >sequence of statements up to that point, followed by execution of the >handler for that exception, establishes the precondition. In fact, >because of RM 11.6, such an intricate approach is futile: ... In the case of predefined exceptions, this is quite true. But 11.6 does not apply to user-defined exceptions, so you can reason about them much more precisely. >...Just because >some subexpression within a statement can raise an exception does not >mean that all the preceding statements have been executed when it does >so! One can prove very little about the state of the computation at the >moment an exception arises. > >Because of RM 11.6, one should not write handlers that depend too heavily >on the state of the computation when the handler is entered. Taken to >its extreme, this principle means that a handler should be written so >that it is possible to prove that it establishes the required >postcondition >>>regardless of the state of the computation upon entry to >the handler<<<. Well, this makes exception handlers pretty useless, since you can't do much of anything in a handler, that depends on much of anything. That is, if you have to prove that "True" implies the post-condition, then the post-condition will necessarily be pretty weak. And, in fact, exception handlers for the predefined exceptions *are* pretty much useless, given 11.6. There are *some* things you can safely do, but it's not easy to tell what. (How many programmers even understand 11.6?! Even language lawyers are confused by it. I know *I* am.) A simple rule of thumb is, "don't handle predefined exceptions". User-defined exceptions are easier to deal with, but you need some way of telling which exceptions can be raised by any subprogram. A "clean-up" exception handler is also easier to deal with ("when others => Clean_Up; raise;"). Here's a case where you very well might be able to prove that Clean_Up works, despite the fact that it's precondition is "True". And in this case, you don't need to prove anything about the post-condition of the containing block. >In fact, one need not be so extreme: One can rely on the values of >variables upon entry to the handled sequence of statements if those >variables are never altered within the handled sequence. Right. - Bob