The definition of data refinement between datatypes is expressed in terms of all programs that
invoke procedures of the types. As a result it is laborious to check. Simulations provide sound
conditions that, being ‘static’, facilitate checking; but then their soundness is important. In
this paper we extract a technique from the heart of the theory and show it to be equivalent to
data refinement; it plays a key role in establishing properties about simulations in any of the
computational models. We survey the difficulties confronting the theory when the procedures
and invoking programs may contain probabilistic choices, and show that then each of the two
simulation conditions is alone not complete as a rule for data refinement, even if the datatypes
are deterministic (in contrast to the standard case). The last part of the paper discusses work
in progress.