Auxiliary variables in data refinement (Q1114384)

A set of local variables in a program is auxiliary if its members occur only in assignments to members of the same set. Data refinement transforms a program, replacing one set of local variables by another set, in order to move towards a more efficient representation of data. Most techniques of data refinement give a direct transformation. But there is an indirect technique, using auxiliary variables, that proceeds in several stages. Usually, the two techniques are considered separately. It is shown that the several stages of the indirect technique are themselves special cases of the direct one, thus unifying the separate approaches. Removal of auxiliary variables is formalized incidentally.