Specifying Program Semantics Precisely and Hierarchically: Consequences

Authors:Koeritz, C, Department of Computer ScienceUniversity of Virginia Knight, J, Department of Computer ScienceUniversity of Virginia

The proper handling of exceptional conditions is important in computing systems that are intended to be dependable. The Ada language is used for programming such systems and provides exception semantics as a means for handling exceptional conditions, but the mere semantics do not guarantee any properties of dependability. Numerous unusual situations (called anomalies here) can exist in the exception handling portions of an Ada program that cause the program to diverge from its specification, often in a completely unacceptable manner. To increase dependability in existent Ada programs, anomalies must be located and removed from them. When implementing new Ada programs, anomalies should be‘ precluded from the system by applying exception handling design principles during program construction. Initially it was believed that these two goals (detection and prevention of anomalies) were sufficient to substantially increase dependability in Ada programs, but now it is felt that the anomalies of Ada arise due to basic problems with the nature of exception handling itself. it is asserted that exception handling is a fundamentally flawed paradigm and that it is not sufficient for the needs of dependable computation. This paper urges a revision of the notions upon which exception handling is based. A new and fundamentally different view of the problem domain currently addressed by exception handling techniques is presented. A model based on the consequence is discussed as an implementable and useable method for addressing the needs of dependable computation. A consequence's intent and causes are more precisely specified than for exceptions, and the consequence is a more general and flexible mechanism than the exception. The consequence model forms the basis for the OZ specification notation. This notation can be added to Ada programs to guarantee properties of their behavior, even if . certain classes of anomalies are present in the implementation. Augmenting an Ada program with accurate OZ specifications also embeds important information in the program's specification that can be used later for verification. Using ‘OZ, certain properties of dependability can be guaranteed a priori; exception handling only begins to afford similar assurance after a difficult and potentially impossible verification of the ad hoc programming employed to handle exceptions. © and last revised January 21, 1993
Note: Abstract extracted from PDF file via OCR

All rights reserved (no additional license for public reuse)
Source Citation:

Koeritz, C, and J Knight. "Specifying Program Semantics Precisely and Hierarchically: Consequences." University of Virginia Dept. of Computer Science Tech Report (1993).

University of Virginia, Department of Computer Science
Published Date: