1990 Reports

Understanding Data Refinement Using Procedural Refinement

Kearns, Steven M.

Data refinement is converting a program that uses one set of variables to an equally correct program that uses another set of variables, usually of different types. There have been a number of seemingly different mathematical definitions of data refinement. We present a unifying view of data refinement as a special case of procedural refinement, which is simpler to understand. All the data refinement theories in the literature are shown to be instances of two formulas, but we show that there are actually an infinite number of theories. In addition, we introduce the concepts of nonlocal data refinement, data refinement using semi-invariants, and procedural optimization using data refinement.