Promotion as a technique for structuring Z specifications appeared as early as the first edition of [107], and there are extensive examples documented (see, for example, [15,209,150]). The definition of freeness is due to Woodcock [207] and work on refinement of promotions goes back to [150].
In [150] Lupton defines the conditions which are sufficient for the
distribution of refinement through promotion and proves the result for
downward simulations. Upward simulations were not considered in
[150].
More recently, Mahony [153] has considered how the structuring
technique of promotion can be embedded within the
refinement calculus notation.