A Logic for Schema-Based Program Development
Martin C. Henson, Steve Reeves · Formal Aspects of Computing · 2003
Abstract. 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 a Z-like specification language, 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.