An Axiomatic Approach to Equivalence of Straight-Line Programs with Structured Variables
University of Wisconsin-Madison Department of Computer Sciences
MetadataShow full item record
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.