Enhancing the Established Strategy for Constructing a Z Specification

Abstract

The Established Strategy for drawing up a Z specification document focuses on a more abstract activity of specification, namely, how to combine schemas but is largely silent about how to construct a schema. Schema construction may benefit from the application of certain heuristics for establishing its content. While formal specification can be seen as a subsection of software engineering and design heuristics in this area are firmly in place, corresponding principles and strategies for constructing a formal specification have been relatively rare. In this paper we examine a number of formal specifications written in Z as well as some design principles from software engineering and areas of general design. On the strength of these, we propose a preliminary set of heuristics for the construction of a formal specification and show how these may be embedded in an enhanced strategy for specification work. We illustrate how one such enhancement, namely the use of primitives, allows a specifier to discharge an important proof obligation arising from a formal specification, where otherwise a proof is not easily arrived at.