CaltechAUTHORS
  A Caltech Library Service

Semantics of Exceptions

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

[img]
Preview
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