THE ROLE OF DATA REIFICATION IN PROGRAM REFINEMENT - ORIGINS, SYNTHESIS AND APPRAISAL

The formal development of implementations from specifications requires that we should be able to justify the replacement of definitions which are clear but inefficient by those which are efficient but unclear. We look at ways to provide such justifications, and see that they depend on the form of the definitions and the ways in which we propose to exploit them. We develop conditions which are feasible to establish and meet the needs of the most common situations, and provide pointers to related work in this area. Some familiarity with set theory will help with the formal definitions, although these can be skipped without loss of continuity.