Self Test: All-points Shortest Paths

Video

An edge-weight matrix \(W\) represents a graph \(G\) in which the weight of edge \(i, j\) is \(W[i,j]\). For all \(j\), \(W[j, j] = 0\). The graph has no cycles of negative length. Let \(sp(W)\) be a matrix of the same dimensions as \(W\) and whose \((i, j)\)-th element is the length of the shortest path from vertex \(i\) to vertex \(j\).

Prove that the following loop terminates and that at termination \(D = sp(W)\).

D = W
for all i, j, k:
  D[i,j] + D[j, k] < D[i,k]  ->   D[i,k] = D[i,j] + D[j, k]
    

Self Test: Proof of Correctness

Test 1

Give and prove an invariant of the loop.

Test 2

Prove that the loop terminates by giving a variant function for the loop.

Test 3

Show that the specification holds upon termination of the loop.

Answers

Answer 1

An invariant of the program is:

\(D \leq W\) and
for all \(i, j\): \(D[i,j]\) is the length of a path from \(i\) to \(j\).

Proof

The predicate holds initially because \(D = W\). The proof that the execution of every command maintains the predicate is straightforward.

Answer 2

\(D\) itself is a variant function. The proof is as follows.

For each \(i, j\), there exist only a bounded number of values for \(D[i,j]\) that satisfy the invariant. This is because there are only a bounded number of cycle-free paths from \(i\) to \(j\). \(D\) is bounded below by the matrix of shortest-path lengths. Therefore \(D\) can decrease only a finite number of times before the lower bound is reached.

The execution of any command with a True guard reduces \(D\). The proof is straightforward.

Answer 3

Next we prove that if the invariant holds and all the guards are false then \(D = sp(W)\) where \(sp(W)\) is the matrix of lengths of shortest paths.

We prove the result by induction on \(m\), the number of hops in shortest paths between vertices. The result holds for shortest paths consisting of a single hop, i.e. if the shortest path from \(i\) to \(j\) is along edge \(i, j\) then:

\( D[i, j] = sp(W)[i, j] \).

Assume that the result holds for all shortest paths with \(m\) hops and prove that it holds for shortest paths with \(m+1\) hops. Let the shortest path from \(i\) to \(k\) take \(m+1\) hops. Let \(j\) be the prefinal vertex on this shortest path. Then

\( sp(W)[i,k] = sp(W)[i,j] + sp(W)[j, k] \) The result follows from the induction assumption.

---

K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology