Proof theory for exception handling in a tasking environment

Abstract

In this paper, we develop a syntax-directed proof system for a fragment of Ada consisting of the essential features of tasking and exception handling. The proof system is based on a correctness formula for therobust specification of single-entry-multiple-exit structures that provides a unified framework for exception handling mechanisms in the presence of nondeterminism, concurrency and communication. The proof system uses the technique ofco-operating proofs, which was developed for proving the correctness of communicating sequential processes [AFD80] and extended to a concurrent fragment of Ada in [GD84]. We build upon the latter. The soundness and completeness are established formally in [Lod87]. The proof rules are structured so that exceptions can be used as a structured escape mechanism in accordance with the design objectives of Ada. Examples are given to show how the rules highlight the annotation required for establishing the robustness of Ada programs.