Programming Research Group Technical Monograph PRG-79

Steve King

February 1990, 25 pages, ISBN 0-902928-57-9

Z has been developed as a formal specification notation, and, as such, has been used successfully for a number of years. Recently, other formal notations, the various flavours of refinement calculi, have emerged. They have been designed as wide spectrum languages to support the whole of the development cycle, from abstract specification through to executable code. We explore the differences between Z and the refinement calculus, and explain the reasons for some of those differences.

We also explain how a development might use both notations, thus giving a path to code from a Z specification. Some rules for switching between the notations are given, and their use is illustrated in a case study.