Proof theory for exception handling in a tasking environment

Lodaya, K. ; Shyamasundar, R. K. (1990) Proof theory for exception handling in a tasking environment Acta Informatica, 28 (1). pp. 7-41. ISSN 0001-5903

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Article
Source:Copyright of this article belongs to Springer.
ID Code:56568
Deposited On:24 Aug 2011 10:57
Last Modified:24 Aug 2011 10:57

Repository Staff Only: item control page