Formal Documentation of Well-Structured Programs

Dr. David Lorge Parnas

Dr. Jan Madey

Mr. Michal Iglewski

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1

Abstract - (revised version of CRL Report No. 259)

This paper introduces a method for making program documentation precise and readable when the program is lengthy. We propose that the program documentation consist of a set of displays supplemented by a lexicon and an index. By a display we mean a document, in which a program fragment is presented in such a way, that its correctness can be examined without looking at other displays. A display consists of three parts: (1) the specification of the program presented in the display, (2) the program itself, in which names of other programs (subprograms) may appear, and (3) the specifications of subprograms invoked by this program. Our technique is a refinement of Mills' functional approach to program documentation and verification; programs are specified by LD-relations represented in tabular form. We illustrate our method on simple examples.