Property-preserving program refinement

During the development and maintenance process, a program changes form, often being refined as specifications and implementation decisions are realized. A correctness proof built in parallel with an original program can be extended to a proof of refined program by showing equivalences between the original and refined program. This paper illustrates two examples of property-preserving refinement, partial evaluation and generalization, and explores the correctness-preserving equivalences underpinning those refinement techniques. We plan to explore ways in which the informal reasoning behind these and similar program refinement tasks may be captured to extend the proof for an original program into a proof of the refined program.