Formal Derivation of Graph AlgorithmicPrograms Using Partition-and-Recur

In this paper,we derive,by presenting some suitable notations,three typical graph algorithms and corresponding programs using a unified approach,partition-and-recur.We putemphasis on the derivation rather than the algorithms themselves.The main ideas and ingenuity 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.

Formal derivation of graph algorithmic programs using partition-and-recur

In this paper, we derive, by presenting some suitable notations, three typical graph aLgorithms and corresponding programs using a unified approach, partition-and-recur. We putemphasis on the derivation rather than the algorithms themselves. The main ideas and lugesnutty of these algorithms are revealed by formula deduction. Success in these examples givesus more evidence that partition-and-recur is a simple and practical approach and developingenough suitable notations is the key in designing and deriving efficient and correct algorithmicprograms.