[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Inferring the Equivalence of Functional Programs that Mutate Data
Mason, I. A. and Talcott, C. L. - 1992

In this paper we study the constrained equivalence of programs with effects. In particular, we present a formal system for deriving such equivalences. The formal system we present defines a single-conclusion consequence relation between finite sets of constraints and assertions. Although the formal system is computationally adequate, even for expressions containing recursively defined functions, it is inadequate for proving properties of recursively defined functions. We show how to enrich the formal system by addition of induction principles. To illustrate the use of the formal system, we give three non-trivial examples of constrained equivalence assertions of well known list-processing programs. We also establish several metatheoretic properties of constrained equivalence and the formal system, including soundness, completeness, and a comparison of the equivalence relations on various fragments.