[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A Sound and Complete Axiomatization of Operational Equivalence Between Programs with Memory
Mason, I. A. and Talcott, C. L. - 1989 - PDF

In this paper we present a formal system for deriving assertions about programs with memory. The assertions we consider are of the following three forms: (i) an expression diverges (i.e. fails to reduce to a value); (ii) two expressions reduce to the same value and have exactly the same effect on memory; and (iii) two expressions reduce to the same value and have the same effect on memory up to production of garbage (are strongly isomorphic). The expressions considered are expressions of a first-order Scheme- or Lisp-like language over a given set of atoms with the data operations ‘atom’ ‘eq’ ‘car’, ‘cdr’, ‘cons’, ‘setcar’, ‘setcdr’, the control primitives ‘let’ and ‘if’, and recursive definition of function symbols. The formal system we present defines a single-conclusion consequence relation between finite sets of constraints and assertions. A constraint is an atomic or negated atomic formula in the first-order language consisting of equality, the unary function symbols ‘car’ and ‘cdr’, the unary relation ‘atom’, and constants from the set of atoms. Constraints have the natural first-order interpretation. The semantics of the formal system is given by a semantic consequence relation which is defined in terms of a class of memory models for assertions and constraints. The main results of this paper are: (Soundness) The deduction system is sound — if the formal proves that an assertion is a consequence of some set of constraints then the assertion is a semantic consequence of that set of constraints. (Completeness) The deduction system is complete for assertions not containing recursively defined function symbols — if such an assertion is a semantic consequence of a set of constraints then it is derivable in the formal system.