## Verification of Programs that Destructively Manipulate
Data

**I. Mason**
*Abstract:* We investigate various equivalence relations
between expressions in a first order functional programming
language augmented with the ability to destructively alter the
underlying data. To define the semantics we introduce the notion of
a memory structure. A computation theory for a lexically scoped
functional language is then defined over these structures. The
equivalence relations are then defined within this model theoretic
framework. A distinction is made between intensional relations and
extensional relations. The former class turn out to have a much
more manageable theory than the latter. The principal intensional
relation studied is strong isomorphism, its properties allow for
elegant verification proofs in a style similar to that of purely
applicative languages. In particular the relation is preserved
under many standard syntactic manipulations and
transformations.

*LFCS report ECS-LFCS-87-40*

Previous |

Index |

Next