Safe|A Semantic Technique for Transforming Programs in the Presence of Errors

Language designers and implementors have avoided specifying and preserving the meaning of programs that produce errors. This is apparently because being forced to preserve error behavior severely limits the scope of program optimization, even for correct programs. However, preserving error behavior is desirable for debugging, and error behavior must be preserved in any language that permits user-generated errors (i.e., exceptions). This paper presents a technique for expressing general program transformations for languages that possess a rich collection of distinguishable error values. This is accomplished by dening a higher-order function called \Safe", which can be used to annotate those portions of a program that are guaranteed not to produce errors. It is shown that this facilitates the expression of very general program transformations, eectively giving program transformations in a language with many error values the same power and generality as program transformations in a language with only a single error value. Using the semantic properties of Safe, it is possible to provide some useful sucient conditions for establishing the correctness of transformations in the presence of errors. In particular, a Substitutability Theorem is proven, which can be used to justify \in-context " optimizations| transformations that alter the meanings of subexpressions without changing the meaning of the whole program. Finally, the eectiveness of the technique is demonstrated by some examples of its use in an optimizing compiler