An axiomatic treatment of exception handling in an expression-oriented language

1 July 1987

journal article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems

Vol. 9 (3) , 390-407
https://doi.org/10.1145/24039.24052

Abstract

An axiomatic semantic definition is given of the replacement model of exception handling in an expression-oriented language. These semantics require only two new proof rules for the most general case. An example is given of a program fragment using this model of exception handling, and these rules are used to verify the consistency of the fragment and its specification.

Keywords

This publication has 10 references indexed in Scilit:

Side effects and aliasing can have simple axiomatic descriptions
ACM Transactions on Programming Languages and Systems, 1985
A modular verifiable exception handling mechanism
ACM Transactions on Programming Languages and Systems, 1985
A mechanism for exception handling and its verification rules
Computer Languages, 1982
Ada exception handling: an axiomatic approach
ACM Transactions on Programming Languages and Systems, 1980
Rationale for the design of the Ada programming language
ACM SIGPLAN Notices, 1979
Axiomatic approach to side effects and general jumps
Acta Informatica, 1977
Exception handling
Communications of the ACM, 1975
Revised report on the algorithmic language ALGOL 68
Acta Informatica, 1975
Program proving: Jumps and functions
Acta Informatica, 1972
An axiomatic basis for computer programming
Communications of the ACM, 1969