Re: Help with Exceptions!

[bobduff@world.std.com (Robert A Duff)]

In article <4nd7cm$fnp@watnews1.watson.ibm.com>,
Norman H. Cohen <ncohen@watson.ibm.com> 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