Changing data representation in the refinement calculus
R. J. R. Back · 2003
It is shown how to change the data representation in programs (data refinement) systematically within refinement calculus. Data refinement in the original refinement calculus was only defined for functional data abstractions. It is shown how the method can be extended to nonfunctional data abstraction by adding 'don't know' (or angelic) nondeterminism to the usual 'don't care' (or demonic) nondeterminism. The method is very flexible, permitting different data abstractions to be combined in the same statement, as well as refinements of the data abstractions themselves. The flexibility is illustrated by an example program derivation.>