Toward modular verifiable exception handling

Recognizing that an error condition is an intrinsic part of the abstract type to which the operation that detects the condition belongs, an attempt is made to specify and implement error condition detection and handling within the framework of the Alphard form, a construct for encapsulation of data...

Full description

Saved in:
Bibliographic Details
Published in:Computer languages 1980, Vol.5 (2), p.77-101
Main Authors: Berry, D.M., Kemmerer, R.A., von Staa, A., Yemini, S.
Format: Article
Language:English
Subjects:
Assertions
Exception handling
Modularity
Software engineering
Structured programming
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recognizing that an error condition is an intrinsic part of the abstract type to which the operation that detects the condition belongs, an attempt is made to specify and implement error condition detection and handling within the framework of the Alphard form, a construct for encapsulation of data type specification and implementation. The essence of the problem is this: while error condition detection is done by the operation in the form, only the user of the type can determine the meaning of the condition with respect to the way the type is used. Thus, the user must be able to specify the handler. Unfortunately, programming the handler often requires access to encapsulated implementation details which are hidden from the user. After discussing the general issues of exception handling, modularity, and abstract data types, this paper proposes a solution for one category of exceptions, namely errors. Specifically an externally visible condition name is the link between an error's occurrence and some externally visible but internally programmed handler for it. Issues raised by this partial solution, including those of proof rules, are discussed.
ISSN:0096-0551
DOI:10.1016/0096-0551(80)90049-1