In Chapter 1 we saw that abstraction relations, rather than abstraction functions, are the natural concept to formulate proof principles for establishing data refinement, i.e., simulation. This impression was reinforced in Chapter 4 by establishing completeness of the combination of L- and L−1-simulation for proving data refinement. How then is it possible that such an apparently practical method as VDM promotes the use of total abstraction functions instead? Notice that in our set-up such functions are the most restrictive version of abstraction relations, because for them the four versions of simulation are all equivalent. Should this not lead to a serious degree of incompleteness, in that it offers a much weaker proof method than L-simulation, which is already incomplete on its own? As we shall see in this chapter this is not necessarily the case. Combining total abstraction functions with so-called auxiliary variables allows the formulation of proof principles which are equal in power to L- and L−1-simulation. Auxiliary variables are program variables to which assignments are added inside a program not for influencing the flow of control but for achieving greater expressiveness in the formulation of abstraction functions and assertions. Following [AL91] such total abstraction functions are called refinement mappings. The chances for an abstraction relation (from a concrete data type to an abstract data type) to be functional can be increased by artificially inflating the concrete level state space via the introduction of auxiliary variables on that level.

By recording part of the history of a computation in an auxiliary variable, called a history variable, and combining this with refinement mappings, a proof method equivalent to L-simulation is obtained.