Simulation as a Proof Method for Data Refinement

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 inves... View More