Introduction:

The traditional set of data refinement rules for Z are stated in [ Spivey 1992 , section 5.6]. These are sufficient to prove many data refinements that occur in practice, but not all. In the late 1990s we performed the specification and full refinement proof of a large, industrial scale application, that of an Electronic Purse [ Stepney et al . 2000 ]. In the course of this work we discovered that the traditional rules were not sufficient to prove our particular refinement. In particular, the traditional obligations assume the use of a 'forward' (or 'downward') simulation, which was inappropriate for our application. We developed a more widely applicable set of Z data refinement proof obligations, for use on our project. These obligations allow both 'forward' and 'backward' simulations [ Woodcock & Davies, 1996 , chapter 16], and also allow non-trivial initialisation, finalisation, and input/output refinement [ Stepney et al . 1998 ].

This monograph, originally produced as part of the Electronic Purse development project, provides the full derivation of these rules for refinement in Z. It covers both the traditional forwards and the new backwards refinement proof rules, and the input/output refinement rules.

The purpose of this monograph is threefold:

1. to make explicit the simplifying assumptions that go into deriving these rules
2. to provide enough working that the source of our derivations is clear
3. to provide enough working that other rules can more readily be derived when making different assumptions

@techreport(SS-YCS-347,
  author = "David Cooper and Susan Stepney and Jim Woodcock",
  title = "Derivation of {Z} Refinement Proof Rules:
           forwards and backwards rules incorporating input/output refinement",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-347",
  month = dec,
  year = 2002
)