Correctness-preserving program transformations

ABSTRACT

This paper extends the predicate calculus formalization of the partial correctness properties of programs (Ki, Go) to include the preservation of correctness under program transformations. The general notion of "program transformations which preserve properties" is fundamental to the theory of programming and programming languages. In the context of proofs of program correctness, transformations which preserve correctness can be used to improve less efficient, but easier to prove, programs. The basic argument in the use of correctness-preserving program transformations (hereafter CPTs) is:Assume that G is a program (with attached assertions) which has been proved correct with respect to some input-output relation Ain-Aout. Now suppose that S is some part of G, e.g. an expression, assertion, statement, etc., which is to be replaced by some other such part S' to produce the program G'. The goal is to prove that G' is also correct with respect to Ain-Aout and therefore the replacement preserves overall program correctness. Moreover, if the replacement has only a local effect, e.g. the body of a loop, then the proof of correctness-preservation should be restricted to that part of the program affected by the replacement.Section 2 reviews the current paradigm for proving program correctness. An example in section 3 illustrates CPTs in a sequence of improvements on a correct and simple, but inefficient, initial program. In section 4, the formalization of partial correctness properties of programs is recast as a semantic language definition using Knuth's semantic method (Kn1). This formalization is then used in section 5 to describe the mechanics of performing CPTs. In section 6, several questions about the formalization of sections 4 and 5 are discussed and a generalization is proposed. Finally, section 7 returns to a concrete example and suggests that the most effective use of CPTs is by identification of schematic forms. Related work is mentioned in section 8.

REFERENCES

• 1: (Bu) Burstall, R. M. "Proving properties of programs by structural induction," Computer Journal 12, (1969), 41-48.
• 2: (DB) Darlington, J., and R. M. Burstall. "A System which automatically improves programs," Proc. 3rd Intl. Conf. on Artificial Intelligence, 479-485.
• 3: (De) Deutsch, L. P. "An interactive program verifier," Ph.D. thesis, Univ. of California, Berkeley, 1973.
• 4: (Di) Dijkstra, E. W. "A simple axiomatic basis for programming language constructs," EWD 372, Eindhoven, May, 1973.
• 5: (Fl) Floyd, R. W. "Assigning meanings to programs," Proc. Symp. Appl. Math., Amer. Math. Soc., Vol. 19, 1967.
• 6: (Ge) Gerhart, S. L. "Knowledge about programs: a model and case study," forthcoming technical report, Duke U.
• 7: Donald Irvin Good, Toward a man-machine system for proving program correctness, 1970
• 8: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 9: (Ho2) Hoare, C. A. R. "Proof of correctness of data representations," Acta Informatica 1, 271-281.
• 10: James Cornelius King, A program verifier, 1970
• 11: (Kn1) Knuth, D. E. "Semantics of context-free languages," Math. Systems Theory 2, 2, 127-145.
• 12: (Kn2) Knuth, D. E. "Examples of formal semantics," Lecture Notes in Mathematics, Vol. 188, E. Engeler, Ed., Springer-Verlag, 212-235.
• 13: (Kn3) Knuth, D. E. "Structured programming with GOTO statements," Stanford University Report STAN-CS-74-416, May, 1974.
• 14: Robin Milner, An algebraic definition of simulation between programs, Stanford University, Stanford, CA, 1971
• 15: (We) Wegbreit, B. "Multiple evaluators in an extensible programming system," FJCC 1972, 905-915.