Lutz, Earlin D.2007-04-232007-04-231989-09http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1041https://hdl.handle.net/1813/6841Three 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.658812 bytes188767 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report