An Axiomatic Approach to Equivalence of Straight-Line Programs with Structured Variables

Abstract

A program scheme which models straight line code admitting structured variables such as arrays, lists, queues, etc. is considered. A set of expressions is associated with a program reflecting the input-output tranformations. A basic set of axioms is given and program equivalence is defined in terms of expression equivalence. Program transformations are then defined such that two programs are equivalent if and only if one program can be transformed to the other via the transformations. An application of these results to code optimization is then discussed.