Using mathematics to specify software
Ian J. Hayes · 1986
When we try to understand computing systems we tend to build a mental model of the system. We use this model to predict the behaviour of the system in untested circumstances. Such mental models are useful but are usually limited because we cannot communicate them directly to other people, and more often than not the model is imprecise. The approach to specification described in this paper is to build a mathematical model of the system being specified. Mathematics provides a mechanism for writing down a precise model that can be communicated to others. Perhaps it should be noted that the main use of a specification is for communication between people, between users and implementors, between managers and programmers. Often communication problems occur because the language in use cannot express the desired information. To be able to write down and make precise the model of a system in a designer’s head will go a long way to communicating to both the users and the implementors what the designer intended. The mathematical model of a system should be abstract and not encumbered with algorithmic details that should be considered part of an implementation. This has the dual advantages that the specification is independent of its implementation(s), and because the designer is describing his system in abstract terms, the system is likely to be simpler; by simpler we mean simpler to understand and to use and not necessarily simpler to implement