Literate specifications

The increasing scale and complexity of software is imposing serious burdens on many industries. Formal notations, such as Z, VDM and temporal logic, have been developed to address these problems. There are, however, a number of limitations that restrict the use of mathematical specifications for large-scale software development. Many projects take months or years to complete. This creates difficulties because abstract mathematical requirements cannot easily be used by new members of a development team to understand past design decisions. Formal specifications describe what software must do; they do not explain why it must do it. In order to avoid these limitations, a literate approach to software engineering is proposed. This technique integrates a formal specification language and a semi-formal design rationale. The Z schema calculus is used to represent what a system must do. In contrast, the `questions, options and criteria´ (QOC) notation is used to represent the justifications that lie behind development decisions. Empirical evidence is presented that suggests the integration of these techniques provides significant benefits over previous approaches to mathematical analysis and design techniques. A range of tools is described that have been developed to support our literate approach to the specification of large-scale software systems