We consider the original work of C. A. R. Hoare and C. B. Jones on data refinement in the light of E. W. Dijkstra and Smyth's treatment of nondeterminism and of Milner and Park's definition of the simulation of Communicating Systems. Two proof methods are suggested which we hope are simpler and more general than those in current use. They are proved to be individually sufficient for the correctness of refinement and together necessary for it. The proof methods can be employed to derive the weakest specification of an implementation from its abstract specification.