Transforming imperative programs
Martin Illsley · ERA · 1988
This thesis describes methods for transforming imperative programs.These transformations are semantics preserving and therefore provide a means of producing a correct efficient program from an inefficient but clear program.Although imperative programming languages are more widely used than functional ones, much more transformation work has been done for the latter.This is mainly because of the more complex nature of imperative programming languages.We extend the usual notion of transformation by introducing a transformation rule, in addition to axioms.This rule is strongly related to the fixed-point characterization rule for the while construct.Whereas transformation axioms have side conditions to restrict their instantiations, our transformation rule has a conclusion which is dependent upon another transformation being possible.That is, if A,B,C,D are programs, in addition to the axiom form of transformation, "A transforms to B", we introduce the rule form of transformation, "if A transforms to B then C transforms to D".We generalise this rule to be context-specific.We have implemented our transformation system, and we give many examples.As a strong indication of the power of the system we prove that a subset of it is sufficient to derive the usual Hoare's logic.This involves setting up a correspondence between bare triples and semantic equivalences.We also discuss the relationship between our system and the Unfold/Fold (UF) system of Burstall and Darlington.We derive a subset of our system using UF via a translation system, but argue that to be a fair comparison we must include a notion of relatively reasonable translation.great insight and tolerance.