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

We present a methodology for the formal spectficataon and development of software systems ustng Z and the refinement calculus. The methodology combmes the data structuring capabdtttes and the codtfied dtscrete mathematics of Z unth the data encapsulation properties and development style of the refinement calculus, and it aims to provide a formal path from design to tmplemen-tatton unthout unnecessary transformations of notatton or the dejinitton of a new calculus. It M illustrated here by the development of two systems, a simple dtary and (part of) a text edztor, and is contrasted wzth the use of Z on its own. We discuss related and future work and conclude with some general comments on applied formal methods.