Some Proofs of Transforms
E. Lutz · eCommons (Cornell University) · 1989
Three simple examples of data refinement-replacement of an abstract program fragment and its variables by a more concrete fragment and variables-are presented in the Polya transform notation. Correctness of each transformation is derived using the formulations of Prinz-Gries, Morris, and Chen/Udding, which are formally equivalent but require different proof strategies. This allows comparison of the three formulations based on ease of use.