Enhancing the Established Strategy for Constructing a Z Specification
Loading...
Authors
Van der Poll, John A.
Kotze, Paula
Issue Date
2005
Type
Article
Language
en
Keywords
Automated reasoning , Established Strategy , Formal specification , Heuristics , OTTER , Primitives , Set theory
Alternative Title
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.