A formalization of superposition refinement

One form of program refinement is to add new variables to the state, together with code that manipulates these new variables. When the addition of new variables and associated computation code is done in a way that prevents the old computation of the program from being disturbed, then the author calls it superpositioning. He studies superposition in the context of constructing parallel programs following the stepwise refinement approach, where the added computation in each step could consist of an entire parallel algorithm. Hence, it is important to find methods that are easy to use and also guarantee the correctness of the operation. It is also important be able to superpose one algorithm, like a termination detection algorithm, onto several different original algorithms. He therefore gives a method for defining and using such superposable modules