Skip to main content

A REFINEMENT CALCULUS FOR Z

Ana Cavalcanti

Abstract

The lack of a method for developing programs from Z specifications is a difficulty that is now widely recognised. As a contribution to solving this problem, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. Other refinement techniques have been proposed for Z; ZRC builds upon some of them, but distinguishes itself in that it is completely formalised.

Institution
OUCL
Month
August
Number
PRG123
Pages
196
Year
1997