ZRC swMATH ID: 21827 Software Authors: Cavalcanti, A.L.C., Woodcock, J.C.P. Description: ZRC - A Refinement Calculus for Z. The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem. As an answer to that, we present ZRC, a refinement calculus based on Morgan’s work that incorporates the Z notation and follows its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC. We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z. Homepage: https://link.springer.com/article/10.1007/s001650050016 Related Software: Circus; Z; ProofPower; ClawZ; ArcAngelC; Simulink; ArcAngel; CirCUs; Z/EVES; Rodin; StateFlow; SPARK; PVS; Daikon; Isabelle/HOL; ML; Hume; Cambridge LCF; Matlab; Haskell Cited in: 11 Publications all top 5 Cited by 11 Authors 10 Cavalcanti, Ana 5 Woodcock, James C. P. 4 Zeyda, Frank 3 O’Halloran, Colin 3 Oliveira, Marcel 2 Clayton, Phil 1 Dunne, Steve E. 1 Guttmann, Walter 1 King, Steve F. 1 Wei, Kun 1 Wellings, Andy Cited in 4 Serials 7 Formal Aspects of Computing 1 Science of Computer Programming 1 Real-Time Systems 1 The Journal of Logic and Algebraic Programming Cited in 1 Field 11 Computer science (68-XX) Citations by Year