CSM-361 - A Logic for Schema-based Program Development
Martin C. Henson, Steve Reeves · Open Access at Essex (University of Essex) · 2001
We show how a theory of specification refinement and program development can be constructed as a conservative extension of our existing logic for Z. The resulting system can be set up as a development method for Z, or as a generalisation of a refinement calculus (with a novel semantics). In addition to the technical development we illustrate how the theory can be used in practice.