Towards design guidelines for constructing a formal specification

Abstract

Accepted software engineering design principles are well established, but design principles 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 strenght of these, we propose a preliminary set of guidelines for the construction of a formal specification. The purpose of these guidelines is to incorporate general design principles as well as those often used in the final software, already at the specification phase. We illustrate how one of these guidelines, naemly the use of primitives, allows a specifier to discharge an important proof obligation arising from a formal specifier to discharge an important proof obligation arising from a formal specification, where otherwise a proof is not easily arrived at.