Combining Algebraic and Algorithmic Reasoning: An Approach to the Schorr-Waite Algorithm

Abstract

The basic idea of the Schorr-Waite graph-marking algorithm can be precisely formulated, explained, and verified in a completely applicative (functional) programming style. Graphs are specified algebraically as objects of an abstract data type. When formulating recursive programs over such types, one can combine algebraic and algorithmic reasoning: An applicative depth-first-search algorithm is derived from a mathematical specification by applying properties of reflexive, transitive closures of relations. This program is then transformed in several steps into a fmal procedural version with the help of both algebraic properties of graphs and algorithmic properties reflected in the recursion structure of the program. © 1982, ACM. All rights reserved.