The verified incremental design of a distributed spanning
tree algorithm
In May, 1996, I concluded the construction of a mechanical proof
of the algorithm of Gallager, Humblet, and Spira for the
distributed determination of the minimum-weight spanning tree of
an undirected graph of processes in which all edges have
different weights. See
R.G. Gallager, P.A. Humblet, P.M. Spira:
A distributed algorithm for minimum-weight spanning trees.
ACM Trans. on Programming Languages and Systems, 5 (1983) 66-77.
The proof is made with the theorem prover NQTHM-1992 of Boyer and
Moore, which can be obtained from
nqthm-request@cli.com, Computational Logic, Inc.,
1717 West Sixth Street, Suite 290,
Austin, Texas 78703, USA.
The algorithm, its design, and the construction of its proof
are described in
The event files that can be read and submitted for NQTHM-1992 to
yield the formal proof are
-
ghsAB.events contains the definitions needed to understand
the main theorems and to try the algorithm in NQTHM's
execution environment (827 lines)
-
ghsC.events contains some auxiliary definitions
and lemmas (350 lines)
-
ghsD.events contains the semantic lemmas, a
preparation for the proofs of invariance (894 lines)
-
ghsE.events contains the graph theory (2178 lines)
-
ghsF.events contains the theory needed to eliminate
the ghost variables from the algorithm (574 lines)
-
ghsJR.events contains the layers (Jq) through (Rq), yielding
the main results for safety (11805 lines)
-
ghsSY.events contains the layers (Sq) through (Yq),
the goal, progress, termination, and the preparations
for the conclusions (15335 lines)
-
ghsZ.events contains the final theorems (183 lines)
Latest update: May 1, 2002. Comments and questions are welcome.
Back to my
home page.