Precise software documentation

Computer Scientists have been talking about the use of of object-orientation (under a variety of rubrics) to achieve "separation of concerns" for more than 40 years. In all that time, it has been taken for granted that it was the structure of the program text itself that mattered. Whenever it was felt that additional information was needed it was assumed that this would be closely associated with the program text either as simple comments, as in-line assertions, or "woven" in with the program text using elaborate tools. This talk takes a different position. It argues that for true separation of concerns we need an integrated set of separate documents, some of which are to be read by people who will never read the code, some that describe the structure of the code, and some that describe the behaviour of individual components. It describes a collection of mathematical ideas and notations that make it possible to produce documentation that is both precise and readable. We then describe the use of these documents in testing and inspection. Finally, it discusses the way that other programming paradigms, particularly functional programming, can be used to make these documents more useful.