n South African Computer Journal - Enhancing the established strategy for constructing a Z specification : reviewed article
|Article Title||Enhancing the established strategy for constructing a Z specification : reviewed article|
|© Publisher:||South African Computer Society (SAICSIT)|
|Journal||South African Computer Journal|
|Author||John A. Van der Poll and Paula Kotze|
|Publication Date||Dec 2005|
|Pages||118 - 131|
|Keyword(s)||Automated reasoning, Established Strategy, Formal specification, Heuristics, OTTER, Primitives, Set theory and Z|
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.
Article metrics loading...