Using ghost variables to prove refinement

Abstract

We propose a method for proving refinement between programs, based on augmenting the program by ghost (auxiliary) variables and statements that assign values to these variables. We show that, in many cases, this augmentation can replace the need for an explicit refinement mapping from the variables of one system to the private variables of the other system. A novel feature of the proposed methodology is that the expressions assigned to the ghost variables may depend on the future. This may replace the need for prophecy variables that are defined by a decreasing induction and require some version of finite-image hypothesis. We believe that proving refinement by program augmentation leads to a more natural style of refinement and is easier to design and comprehend. Allowing future-dependent expressions in a program requires extensions to the temporal methodology for proving properties of programs. These extensions are explained and discussed in the paper.

This research was supported in part by a basic research grant from the Israeli Academy of Sciences, and by the European Community ESPRIT Basic Research Action Project 6021 (REACT).