10.21 Proving Correctness of Shortest-Path Algorithms

Shortest-path algorithms are easy to implement incorrectly. A program may pass small examples while failing on edge cases involving cycles, unreachable vertices, zero-weight edges, or negative weights.

Correctness proofs prevent this kind of accidental confidence.

This recipe develops the proof patterns used for shortest-path algorithms. The goal is not formal theorem proving. The goal is to learn the invariants that explain why an algorithm returns the right answer.

Problem

Given a shortest-path algorithm, prove that it computes correct shortest-path distances under its stated assumptions.

For example:

BFS requires unweighted edges.
Dijkstra requires nonnegative edge weights.
Bellman-Ford allows negative edges but no reachable negative cycles.

Each algorithm is correct only under its own assumptions.

Solution

Most shortest-path correctness proofs use three ingredients:

Distance labels are upper bounds.
Relaxation preserves valid path costs.
The algorithm eventually makes every relevant shortest path available.

The first two ideas apply almost everywhere.

The third depends on the specific algorithm.

Distance Labels Are Upper Bounds

A distance label:

dist[v]

usually means:

The best path cost to v found so far.

At initialization:

dist[source] = 0
dist[other] = infinity

The label for the source is exact.

The labels for other vertices are safe upper bounds because infinity is larger than any valid finite path cost.

When relaxation succeeds:

candidate := dist[u] + weight

if candidate < dist[v] {
	dist[v] = candidate
}

the new value comes from a real path:

source -> ... -> u -> v

Therefore, every finite distance label always corresponds to an actual path.

This gives the first core invariant:

Every finite dist[v] is the cost of some source-to-v path.

The algorithm never invents a distance that is too small.

Relaxation Preserves Correctness

Relaxation asks whether one known path can be extended by one edge.

If:

dist[u]

comes from a valid path to u, and there is an edge:

u -> v

with weight w, then:

dist[u] + w

is the cost of a valid path to v.

Updating:

dist[v]

with that value is safe.

This is why relaxation-based algorithms are robust. Each update has a concrete witness path behind it.

A proof can repeatedly use this fact.

Proving BFS Correctness

BFS assumes every edge has cost one.

The main invariant is:

Vertices are dequeued in nondecreasing distance from the source.

When the source is enqueued, its distance is zero.

All neighbors discovered from it receive distance one.

All undiscovered neighbors of those vertices receive distance two.

The queue preserves this layer order.

To prove correctness, suppose BFS first discovers vertex v with distance k.

If a shorter path existed, it would have length less than k.

That path would end with an edge from some vertex at distance less than k.

BFS would have processed that earlier layer before assigning distance k to v.

So v would already have been discovered.

Contradiction.

Therefore, the first distance assigned by BFS is optimal.

Proving Dijkstra Correctness

Dijkstra assumes all edge weights are nonnegative.

The main invariant is:

Every settled vertex has its final shortest-path distance.

A vertex becomes settled when it is removed from the priority queue with the smallest tentative distance.

Suppose Dijkstra settles vertex v.

Assume for contradiction that a shorter path to v exists.

Follow that path from the source. It must eventually cross from a settled vertex to an unsettled vertex.

Let that crossing edge be:

x -> y

where x is settled and y is unsettled.

When x was settled, Dijkstra relaxed x -> y.

So:

dist[y]

is at most the cost of the prefix path to y.

Because all remaining edge weights are nonnegative, the full path to v cannot be cheaper than that prefix.

So some unsettled vertex on the path has distance less than dist[v].

But Dijkstra selected v as the unsettled vertex with minimum tentative distance.

Contradiction.

Therefore, dist[v] is final when v is settled.

Proving Bellman-Ford Correctness

Bellman-Ford allows negative edges.

It does not settle vertices greedily.

Instead, it relies on path length.

The key invariant after i passes is:

After i full relaxation passes, dist[v] is no larger than the cost of any source-to-v path using at most i edges.

Base case:

i = 0

Only the source has a zero-edge path to itself.

Inductive step:

Suppose the claim holds after i - 1 passes.

Take any shortest path with at most i edges:

source -> ... -> u -> v

The prefix path to u has at most i - 1 edges.

By the induction hypothesis, dist[u] is no larger than that prefix cost.

During pass i, Bellman-Ford relaxes edge:

u -> v

so dist[v] becomes no larger than the cost of the whole path.

After V - 1 passes, every simple shortest path has been considered, because a simple path contains at most V - 1 edges.

If no reachable negative cycle exists, some shortest path can be chosen simple.

Therefore, Bellman-Ford computes all shortest-path distances.

Proving Negative-Cycle Detection

After V - 1 passes, all shortest simple paths have been accounted for.

If one more relaxation still improves a distance, then the improving path uses at least V edges.

A path with at least V edges repeats a vertex.

The repeated section is a cycle.

Since the path became cheaper by including that repeated section, the cycle must have negative total weight.

Thus, an improvement on the extra pass proves the existence of a reachable negative cycle.

The reverse direction is also true: if a reachable negative cycle exists, repeated traversal keeps reducing some distance, so relaxation remains possible.

Proving Floyd-Warshall Correctness

Floyd-Warshall uses a dynamic programming invariant.

After processing intermediate vertices:

0, 1, ..., k

the matrix entry:

dist[i][j]

equals the shortest path from i to j whose intermediate vertices are drawn only from that processed set.

When considering vertex k, a shortest path from i to j either:

does not use k

or:

uses k

If it uses k, it decomposes into:

i -> k
k -> j

So the update:

dist[i][j] = min(
	dist[i][j],
	dist[i][k] + dist[k][j],
)

considers exactly the missing case.

After all vertices have been processed, every possible intermediate vertex is allowed.

The matrix therefore contains all-pairs shortest-path distances.

Proving DAG Shortest Paths Correctness

DAG shortest paths rely on topological order.

In a topological ordering, every edge:

u -> v

places u before v.

When the algorithm processes vertex v, all possible predecessors of v have already been processed.

Therefore all incoming ways to improve dist[v] have already been considered.

No later vertex can lead back to v, because that would create a cycle.

Thus, a single pass in topological order is enough.

This proof is shorter than Dijkstra's because acyclicity gives a stronger structural guarantee.

Common Proof Pattern

Most shortest-path proofs follow the same structure.

First, show that every distance label corresponds to some real path.

Second, show that the algorithm cannot miss a better path.

Third, show that termination occurs after enough relaxations, extractions, or dynamic programming updates.

This pattern works for BFS, Dijkstra, Bellman-Ford, Floyd-Warshall, DAG shortest paths, and many variants.

Implementation Invariants

Correct code should preserve the proof invariants.

For BFS:

A vertex is marked visited when enqueued.

For Dijkstra:

The priority queue is ordered by tentative distance.

For Bellman-Ford:

Every edge is considered during each pass.

For Floyd-Warshall:

The outer loop is the intermediate vertex.

For DAG shortest paths:

Vertices are processed in topological order.

If an implementation violates these conditions, the proof no longer applies.

Testing Against the Proof

Good tests should target the assumptions.

For BFS, include an unweighted graph with multiple equal-length shortest paths.

For Dijkstra, include zero-weight edges and a graph where a later relaxation improves a tentative distance.

For Bellman-Ford, include negative edges and a reachable negative cycle.

For Floyd-Warshall, include unreachable pairs and negative edges without negative cycles.

For DAG shortest paths, include negative edges and disconnected components.

Tests should not merely check happy paths. They should exercise the invariants.

Common Mistakes

Do not prove Dijkstra correct without explicitly using nonnegative edge weights.

Do not prove BFS correct for weighted graphs.

Do not assume Bellman-Ford requires paths with exactly V - 1 edges. It covers paths with at most that many edges.

Do not ignore unreachable vertices in proofs or code.

Do not confuse a distance estimate with a final shortest-path value.

Takeaway

Shortest-path correctness proofs are built from a small set of reusable ideas: distance labels represent real paths, relaxation safely improves labels, and each algorithm schedules relaxations in a way that eventually accounts for every possible shortest path. BFS relies on layers, Dijkstra relies on nonnegative weights and greedy settlement, Bellman-Ford relies on path length, Floyd-Warshall relies on intermediate-vertex dynamic programming, and DAG shortest paths rely on topological order. Understanding these invariants makes implementations easier to trust and easier to debug.