[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Reasoning About Programs with Effects
Mason, I. A. and Talcott, C. L. - 1990

In this paper we give several examples that illustrate our techniques for reasoning about programs with effects. One technique is to define correspondences between effect-free programs and programs with effect and transfer results about effect-free programs to corresponding programs with effects. We give two examples of this technique. The first involves the correspondence between loops and tail-recursive programs, replacing assignment to loop variables by \qlet binding. The second example involves a correspondence between mutable objects and streams, replacing updating by explicitly passing the store. The correspondences are left informal here, but in practice translators can be defined to insure correct correspondences (and avoid the work of hand translation). A second technique is to lift principles for reasoning about effect-free programs to those with effects, typically by finding appropriate abstractions and restrictions. We present three examples here: the use of structure copying to insure non-interference among operations; the use of structural induction principles for establishing program equivalence; and the use of abstract objects to encapsulate effects and potential interference in a controlled way.