Leino, K. Rustan M. and Van de Snepscheut, Jan L. A. (1993) Semantics of Exceptions. Computer Science Technical Reports, 1993.34. California Institute of Technology , Pasadena, CA. (Unpublished) https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-34
![]()
|
PDF
- Submitted Version
See Usage Policy. 480kB |
Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-34
Abstract
We describe a trace semantics of exceptions and then derive a weakest precondition semantics. A program that contains exceptions terminates in one of two possible ways (if it terminates at all): either it terminates exceptionally or it terminates normally. We will therefore consider weakest preconditions that are functions of two postconditions. As a preparation we study aribitrary functions of two arguments, and their compositions.
Item Type: | Report or Paper (Technical Report) |
---|---|
Additional Information: | © 1993 California Institute of Technology. We gratefully acknowledge the contributions made by Robert Harley and Peter Hofstee during various discussions. Also the feedback from Greg Nelson and from other members of IFIP WG 2.3 is greatly appreciated. Although we had not actually seen the paper we were well aware of the semantics for exceptions given in [5], which is identical to the axiomatic semantics given in the present paper. Our trace semantics serves as a foundation thereof. Another early reference to semantics of exception handling is. This reference provides a good discussion of how exception handling can simplify the structure of certain programs. It describes the semantics of exceptions by giving a predicate transformer for normal termination and a separate predicate transformer for exceptional termination. We use one function that maps a pair into a single predicate. |
Group: | Computer Science Technical Reports |
Series Name: | Computer Science Technical Reports |
Issue or Number: | 1993.34 |
DOI: | 10.7907/Z9KK98TT |
Record Number: | CaltechCSTR:1993.cs-tr-93-34 |
Persistent URL: | https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-34 |
Usage Policy: | You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format. |
ID Code: | 26774 |
Collection: | CaltechCSTR |
Deposited By: | Tony Diaz |
Deposited On: | 25 Apr 2001 |
Last Modified: | 03 Oct 2019 03:17 |
Repository Staff Only: item control page