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