Some Proofs of Transforms

Abstract

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.