Development of several reachability algorithms for directed graphs

Abstract

In the development above only the control structure of the algorithms was subject to transformations. The final versions (6) and (7) which are due to the different generalizations in Section 3.1 are both operational provided implementations of the underlying data structures for vertices, graphs, and sets are given.

If these implementations are too inefficient or are not available at all, transformations of the data structures would have to follow. For example, an implementation of graphs by successor lists and of sets by boolean vectors allows to achieve a complexity O(NM) for algorithm (6), where M denotes the number of arcs of the graph. However, using two different set implementations (namely boolean vectors for the argument t and stacks or queues for s) and successor lists for graphs again, we could even obtain an O(M) version of (7). This shows that different strategies and techniques may lead to algorithms of different complexity. But on the other hand, the example also demonstrates that different sequences of design decisions can yield the same result.

Since the derivation of algorithms is a complex and creative task, there is no a priori recipe to determine which strategy or technique is best at a specific stage. Hence, the transformational approach is user-controlled. It offers the programmer various routes to follow and due to the correctness of each individual rule the final program is correct with respect to the initial specification by construction.