Programming Research Group Technical Monograph PRG-125

Jesus N. Ravelo

April 1999, 184 pages

Much emphasis has been placed in recent years on deriving or calculating programs rather than proving them correct. Adequate calculational frameworks are needed to support such an approach. This thesis explores the use of a calculus of binary relations to express and reason about graph-theoretical concepts in the context of program construction. Since graphs play a prominent role in algorithmics and have applications in many other fields, such a calculational treatment of graphs via relations positively benefits the formal construction field.

Phrasing the basics of graph theory with relations allows a compact presentation of well-known facts, as well as the development of novel proofs for such facts in a calculational fashion. Such a machinery is combined with predicate, refinement and fixed-point calculi to derive imperative programs that solve several graph computational problems. Relations are used to model graphs and sets as the data manipulated by programs and specifications. The case-studies put forward in this thesis include some generic problems with instances that correspond to graph algorithms as well as some individual graph problems. These examples demonstrate the applicability of the framework of relations to calculational graph algorithmics, yet some drawbacks are examined. Potential sources of improvement of this presentation and hints on future research are discussed.