Formal Program Documentation
Dennis K. Peters · 1996
The display method is a technique for documenting the design of a program and presenting it such that it can be reviewed in small, independent pieces. This paper uses the display method to present a reasonably complicated program: an implementation of Dijkstra’s ‘shortest path algorithm’. The number of displays required to document a program can sometimes be reduced by using procedure specifications instead of program specifications, as is done in previous work using the display method. When writing procedure specifications care must be taken to describe the required behaviour under aliasing conditions. A discussion of specification s for C functions is given.