Dijkstra's algorithm: a proof of correctness

Problem setup and notation

Let G = (V, E) be a directed, weighted graph with non-negative edge weights w(u, v) ≥ 0, and a source vertex s. Define δ(s, v) as the true shortest-path distance from s to v (the quantity we want to compute). Dijkstra's algorithm maintains, for every vertex v, an estimate d[v] which starts at ∞ (except d[s] = 0) and only ever decreases.

The algorithm

Dijkstra maintains a set S of "settled" vertices (whose shortest distance is finalised) and repeatedly extracts the unsettled vertex u with the smallest d[u], adding it to S, then relaxes every outgoing edge (u, v):

The entire proof of correctness rests on one property of RELAX: it never makes d[v] smaller than δ(s, v) — it can only approach the truth from above, never overshoot below it.

The relaxation invariant

Lemma (upper-bound property): at all times during the algorithm's execution, d[v] ≥ δ(s, v) for every vertex v.

Proof by induction on the number of RELAX calls. Initially d[s] = 0 = δ(s, s) and d[v] = ∞ ≥ δ(s, v) for all other v — the base case holds trivially. Suppose the invariant holds before a call RELAX(u, v, w). If the call changes d[v], the new value is d[u] + w(u, v). By the inductive hypothesis d[u] ≥ δ(s, u), so:

So the invariant is preserved by every RELAX call, and by induction holds throughout execution. This single fact — d never dips below the truth — is the load-bearing wall of the entire proof.

Proof by induction on settled order

Theorem: when Dijkstra's algorithm adds vertex u to S (settles it), d[u] = δ(s, u).

Proof by strong induction on the order in which vertices are settled. Let u be the k-th vertex settled, and assume the theorem holds for the first k − 1 settled vertices.

Consider the true shortest path P from s to u. Let y be the first vertex on P that is not yet in S at the moment u is settled (y = u is possible if the whole path is already settled up to u), and let x be its predecessor on P (x ∈ S, or x = s). Because all edge weights are non-negative, and because x was settled before u, RELAX(x, y, ·) was called when x was settled, so by the invariant proved above:

Now, because edge weights are non-negative, every vertex after y on path P (including u itself) is at least as far from s as y is: δ(s, y) ≤ δ(s, u). But Dijkstra chose u (not y) as the vertex with minimum d-value among all unsettled vertices, so d[u] ≤ d[y] = δ(s, y) ≤ δ(s, u). Combined with the upper-bound lemma d[u] ≥ δ(s, u), we get d[u] = δ(s, u). ∎

The greedy exchange argument

An equivalent, more intuitive way to see the same result: Dijkstra is a greedy algorithm, and greedy algorithms are correct exactly when a "greedy choice property" plus "optimal substructure" both hold.

• Optimal substructure: any sub-path of a shortest path is itself a shortest path between its endpoints — trivially true, since a shorter sub-path would give a shorter overall path.
• Greedy-choice property: among all unsettled vertices, the one with the smallest tentative distance already has its final, correct distance — this is precisely what the induction above establishes.

Because both properties hold under non-negative weights, the exchange argument concludes: replacing the greedy choice with any other choice cannot improve the solution, so the greedy strategy is optimal at every step, and therefore globally optimal.

Why negative weights break the proof

Consider s → a (weight 2), s → b (weight 1), a → b (weight −3). After relaxing both edges out of s, d[a] = 2 and d[b] = 1, so Dijkstra settles b first (smallest tentative distance) — before vertex a, which holds the only edge that could improve b's distance, has even been processed. Once b is settled, the algorithm never relaxes an edge into it again.

Priority-queue implementation

function dijkstra(graph, source) {
  // graph: Map<vertex, Array<[neighbor, weight]>>, all weight >= 0
  const dist = new Map();
  const prev = new Map();
  const settled = new Set();
  const pq = new MinHeap();  // binary min-heap keyed by distance

  for (const v of graph.keys()) dist.set(v, Infinity);
  dist.set(source, 0);
  pq.push(source, 0);

  while (!pq.isEmpty()) {
    const u = pq.pop();          // vertex with smallest tentative distance
    if (settled.has(u)) continue;  // stale heap entry — skip
    settled.add(u);                // u is now permanently finalised

    for (const [v, w] of graph.get(u)) {
      if (settled.has(v)) continue;
      const candidate = dist.get(u) + w;
      if (candidate < dist.get(v)) {   // RELAX step
        dist.set(v, candidate);
        prev.set(v, u);
        pq.push(v, candidate);
      }
    }
  }
  return { dist, prev };
}

Complexity summary

For dense graphs (E ≈ V²) the plain array implementation is actually fastest in practice due to low constant factors. For sparse graphs — the common case in road networks and game maps — the binary-heap version is the standard choice.