A practical approach to software engineering using Z and the refinement calculus

We present a methodology for the formal specification and development of software systems using Z and the refinement calculus. The methodology combines the data structuring capabilities and the codified discrete mathematics of Z with the data encapsulation properties and development style of the refinement calculus, and it aims to provide a formal path from design to implementation without unnecessary transformations of notation or the definition of a new calculus. It is illustrated here by the development of two systems, a simple diary and (part of) a text editor, and is contrasted with the use of Z on its own. We discuss related and future work and conclude with some general comments on applied formal methods. 1 Introduction The use of Z [2, 16] to specify software systems is becoming more and more widespread: IBM has used Z successfully in specifying parts of its CICS transaction processing system [3, 10]; Z has been used to clarify an IEEE floating point standard [1]; there is wor..