## 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) |