Specifying and refining programs with Z

Abstract

The author discusses the need to record design decisions in software development, operation refinement in a development process, the relation between a specification and its refinements, guarded command language, data declarations, specifications as commands, and the use of Z to summarize the function of programs in the guarded command language.