The intended audience for this paper is researchers in semantics and correctness proofs of programs who are interested in languages with exception handling. In the introduction the author distinguishes two kinds of exception handling: the first is an escape mechanism from error situations, as in Ada; the second mechanism allows for termination as well as resumption of the operation that raised the exception.

The paper presents a Hoare-like axiom system to reason about the correctness of programs using exceptions. According to the author, little related work has been published: the main difficulty is the combination of static scope for procedure calling and the dynamic association of handlers with raised exceptions.

In section 2 the author introduces the syntax of the language ℒ _{e x c}. It includes exception raising, together with exception handlers. Formal procedures and recursive handlers are not allowed, however.

In section 3 an informal description of the semantics of the language is presented. ℒ _{e x c} assumes the second kind of exception handling, that is, a handler may either use a terminate statement, thereby exiting the block containing the handler declaration--and all dynamically contained blocks--or (implicitly) resume the operation that raised the exception.

Sections 4 and 5 introduce some definitions, and section 6 presents a formal semantics for ℒ _{e x c}. Sections 7 and 8 form the main dish: the Hoare-like axiom system H for ℒ _{e x c} is introduced, and a proof is presented of the soundness and completeness of H, when we restrict ℒ _{e x c} to certain sublanguages. This main part of the paper is technical and assumes some knowledge of semantic theory. Section 9 presents an example program together with an application of the system H to prove a Hoare-like triple about the program.

The notation is sometimes awkward to read; it needs some polishing. The main problem is the need to distinguish between dynamic occurrences of the same exception identifier. This makes it necessary to introduce a family of countably infinite sets of exception identifiers, clogging up all subsequent formulas and lemmata. The paper succeeds, however, in constructing a Hoare-like system for verification of languages with exception handling that can be used in practical situations.