Formal Derivation of Graph Algorithmic Programs Using Partition-and-Recur

摘要

In this paper, we derive, by presenting some suitable notations, three typical graph al- gorithms and corresponding programs using a unified approach, partition-and-recur. We put emphasis on the derivation rather than the algorithms themselves. The main ideas and inge- nuity of these algorithms are revealed by formula deduction. Success in these examples gives us more evidence that partition-and-recur is a simple and practical approach and developing enough suitable notations is the key in designing and deriving efficient and correct algorithmic programs.