Z AND THE REFINEMENT CALCULUS

Abstract

Z has been developed as a formal specification notation, and, as much, has been used successfully for a. Dumber 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 examine how a development might use both notations, thus giving a path to code from a Z specification. Some rules for switching between the notations axe given, and their use is illustrated in a case study.