Liberating data refinement

Traditional rules for refinement of abstract data types suggest a software development process in which much of the detail has to be present already in the initial specification. In particular, the set of available operations and their interfaces need to be fixed. In contrast, many formal and informal software development methods rely on changes of granularity and require introduction of detail in a gradual way during the development process. This paper discusses several generalisations and extensions of the traditional refinement rules, which are compatible with each other and, more importantly, with the semantic grounding of data refinement. Together they should provide a semantic justification to a larger spectrum of development steps. The discussion takes place in the context of the formal specification language Z and its relational underpinnings.