Mikhajlova and Sekerinski [159] investigated class refinement and interface refinement for object-oriented languages. Their results have very reassuring similarities to ours. First, their ``interface refinement" condition generalises ``class refinement" in much the same way as our IO refinement generalises data refinement. Also, they conclude that sensible input transformers should be surjective, and output transformers functional, which is exactly what we require given that their transformers operate in the opposite direction. Also, the need to administrate the transformers that have been applied so far appears in their notion of ``wrappers".
Work by Stepney, Cooper and Woodcock [193,208] gives a generalisation of standard Z data refinement very similar to that presented here. The main differences are that global state is made explicit in initialisation and finalisation, and the assumption of a notion of global input and output which is separate from the global state itself. The necessary relations between local and global IO correspond to our original IO transformers. More details are expected to appear in a forthcoming book by these authors.
The ideas presented in this chapter were first published in [21].