Deriving efficient graph algorithms (summary)

Ten years ago Hopcroft and Tarjan discovered a class of very fast algorithms for solving graph problems such as biconnectivity and strong connectivity. While these depth-first-search algorithms are complex and can be difficult to understand, the problems they solve have simple combinatorial definitions that can themselves be considered algorithms, though they might be very inefficient or even infinitary. We demonstrate here how the efficient algorithms can be systematically derived using program transformation steps from the initial definitions. This is the first occasion that these efficient graph algorithms have been systematically derived. There are several justifications for this work. First, the derivations illustrate several high-level principles of program derivation and suggest methods by which these principles can be realized as sequences of program transformation steps. Second, we believe that the evolutionary approach used in this paper offers more natural explanations of the algorithms than the usual a posteriori proofs that appear in textbooks. Third, these examples illustrate how external domain-specific knowledge can enter into the program derivation process. Finally, we believe that future programming tools will be semantically based and are likely to have their foundations in a logic of program derivation. By working through complex examples such as those presented here, we make steps towards a conceptual and formal basis for these tools.

Duke Scholars

Author John H. Reif Computer Science