An axiomatic treatment of exception handling in an expression-oriented language
Shaula Yemini, Daniel M. Berry · ACM Transactions on Programming Languages and Systems · 1987
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.