The definition of data refinement given in the previous chapter requires that an infinite number of inclusions should hold, namely one for every choice of program involved. Consequently it does not yield an effective proof method. In this chapter we define such a method, called simulation, and investigate its soundness and completeness w.r.t. the criterion of proving data refinement. In order to define simulation one needs the concept of abstraction relation, relating concrete data values to abstract ones. We briefly discuss why abstraction relations rather than abstraction functions are used, and how data invariants (characterizing the reachable values in a data type) solve one of the problems associated with converting abstraction relations into abstraction functions. Since ultimately proofs are carried out in predicate logic, this raises the question how to express abstraction relations within that logic. As we shall see, this forces us to distinguish between those variables within a program that are unaffected by the data refinement step in question (these are called normal variables) and those that are affected by that step (called representation variables). This raises a number of technical issues which are discussed and for which we present a solution. Next, two methods presently in use for proving data refinement, namely Reynolds' method and VDM, are briefly introduced by way of an example. Finally, we discuss both the distinction between, and the relative values of, syntax-based methods for proving data refinement and semantically oriented ones.