n South African Computer Journal - Enhancing the established strategy for constructing a Z specification : reviewed article




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...

This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error