Derivation of Efficient DAG Marking Algorithms

Abstract

The best known linear-time list marking algorithms also require a linear amount of workspace. Algorithms working in bounded workspace have been obtained only by allowing quadratic execution time or by restricting the list structures to trees. We improve on this here by deriving a new linear-time, bounded workspace marking algorithm that works for dags. The algorithm is derived using correctness-preserving program transformations, which prove the correctness of the algorithm. Our derivation of the marking algorithm provides an example where this method has actually been used to derive a new, more efficient algorithm, rather than just to establish the correctness of a previously known algorithm.