Program derivation through transformations: The evolution of list-copying algorithms

AbstractThe introduction of Hoare Logic made it feasible to supply correctness proofs of small sequential programs. While correctness proofs of larger programs could be given in principle, the increased size of such a proof warranted additional organization. The present paper puts emphasis on the technique of program transformation to show the derivability and to prove the correctness of some fast list-copying algorithms developed by Robson, Fisher and Clark. This subject was motivated by an earlier paper on the same topic by Lee, De Roever and Gerhart. Some transformation rules necessary for the correctness proofs are given. Other proof techniques used include data refinement and the use of auxiliary variables and structures