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.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC 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: ncohen@watson.ibm.com (Norman H. Cohen)
Subject: Re: Help with Exceptions!
Date: 1996/05/15
Message-ID: <4nd7cm$fnp@watnews1.watson.ibm.com>#1/1
X-Deja-AN: 154991802
distribution: world
references: <4mmimq$s4r@hatathli.csulb.edu> <319764DA.3A8C@io.com>
 <EACHUS.96May13172506@spectre.mitre.org>
 <gauthier-1405960958270001@164.81.60.62> <DrEB77.Kwu@world.std.com>
organization: IBM T.J. Watson Research Center
reply-to: ncohen@watson.ibm.com
newsgroups: comp.lang.ada
Date: 1996-05-15T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <DrEB77.Kwu@world.std.com>, bobduff@world.std.com
(Robert A Duff) writes: 

|> In article <gauthier-1405960958270001@164.81.60.62>,
|> Michel Gauthier <gauthier@unilim.fr> wrote: 
|> >...So, I
|> >teach the
|> >rule : for a label, a program end or an exception handler, always establish a
|> >complete list of all gotos or raises and attach the corresponding assertion.
|>
|> This makes good sense for labels/goto's, but I don't think it is
|> reasonable for exception handlers.  The whole point of exception
|> handling is that the code detecting the error, and the code handling the
|> error are separated from each other, and need not know about each other.

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.

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:  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<<<.

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.

--
Norman H. Cohen    ncohen@watson.ibm.com