What is a Good Formal Specification?

Abstract

Most interesting problems can be specified in many different but equivalent ways. Which of these is to be preferred depends on your sense of style. This paper investigates the choices that arise in writing a. formal specification, and suggests some guidelines that may help authors. For reasons of space, only small examples are given. The tension between clarity and brevity is investigated, and it is suggested that clarity must be preferred, though some suggestions are made for writing specifications that are brief but still clear. The most important point is that, if readers of a specification are to have confidence in its integrity, it must contain formal definitions and informal narrative that correspond closely, so that they can be checked. A natural specification is one where the mathematics follows the form of the English description (and not the other way round). The separation between the form of the mathematics and the English is referred to as the “syntactic gap”.