LITERATE SPECIFICATIONS

The increasing scale and complexity of software is imposing serious bu rdens an many industries. Formal notations, such as Z, VDM and tempora l logic, have been developed to address these problems. There are, how ever, a number of limitations that restrict the use of mathematical sp ecifications for large-scale software development. Many projects take months or years to complete, This creates difficulties because abstrac t mathematical requirements cannot easily be used by new members of a development team to understand past design decisions. Formal specifica tions describe what software must do, they do not explain why it must do it. In order to avoid these limitations, a literate approach to sof tware engineering is proposed, This technique integrates a formal spec ification language and a semi-formal design rationale, The Z schema ca lculus is used to represent what a system must do. In contrast, the Qu estions, Options and Criteria notation is used to represent the justif ications that lie behind development decisions, Empirical evidence is presented that suggests the integration of these techniques provides s ignificant benefits over previous approaches to mathematical analysis and design techniques, A range of tools is described that have been de veloped to support our literate approach to the specification of large -scale software systems.