The correctness of the algorithm can be shown by
induction:
Lemma. After
i repetitions of
for loop, • if Distance(
u) is not infinity, it is equal to the length of some path from
s to
u; and • if there is a path from
s to
u with at most
i edges, then Distance(u) is at most the length of the shortest path from
s to
u with at most
i edges.
Proof. For the base case of induction, consider i=0 and the moment before
for loop is executed for the first time. Then, for the source vertex, source.distance = 0, which is correct. For other vertices
u, u.distance =
infinity, which is also correct because there is no path from
source to
u with 0 edges. For the inductive case, we first prove the first part. Consider a moment when a vertex's distance is updated by v.distance := u.distance + uv.weight. By inductive assumption, u.distance is the length of some path from
source to
u. Then u.distance + uv.weight is the length of the path from
source to
v that follows the path from
source to
u and then goes to
v. For the second part, consider a shortest path
P (there may be more than one) from
source to
v with at most
i edges. Let
u be the last vertex before
v on this path. Then, the part of the path from
source to
u is a shortest path from
source to
u with at most
i-1 edges, since if it were not, then there must be some strictly shorter path from
source to
u with at most
i-1 edges, and we could then append the edge
uv to this path to obtain a path with at most
i edges that is strictly shorter than
P—a contradiction. By inductive assumption, u.distance after
i−1 iterations is at most the length of this path from
source to
u. Therefore, uv.weight + u.distance is at most the length of
P. In the
ith iteration, v.distance gets compared with uv.weight + u.distance, and is set equal to it if uv.weight + u.distance is smaller. Therefore, after
i iterations, v.distance is at most the length of
P, i.e., the length of the shortest path from
source to
v that uses at most
i edges. If there are no negative-weight cycles, then every shortest path visits each vertex at most once, so at step 3 no further improvements can be made. Conversely, suppose no improvement can be made. Then for any cycle with vertices
v[0], ...,
v[
k−1], v[i].distance Summing around the cycle, the
v[
i].distance and
v[
i−1 (mod
k)].distance terms cancel, leaving 0 I.e., every cycle has nonnegative weight. == Finding negative cycles ==