Shortest Path Algorithm: Formal Program Documentation

Dennis K. Peters

Abstract

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 specifications for C functions is given.


back to Dennis Peters' homepage

Last modified: Sun 1999.01.03 at 15:29 NST by Dennis Peters