Some Proofs of Transforms
Lutz, Earlin D.
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.
computer science; technical report
Previously Published As