structural:reformatting
Proof of correctness

To prove the correctness of Dijkstra's algorithm, we proceed by mathematical induction on the number of visited nodes.

Invariant hypothesis: For each visited node v, dist is the shortest distance from source to v, and for each unvisited node u, dist is the shortest distance from source to u when traveling via visited nodes only, or infinity if no such path exists. (Note: we do not assume dist is the actual shortest distance for unvisited nodes, while dist is the actual shortest distance)

Base case:

The base case is when there is just one visited node, source. Its distance is defined to be zero, which is the shortest distance, since negative weights are not allowed. Hence, the hypothesis holds.

Inductive step:

Assume the hypothesis holds for k {\displaystyle k} visited nodes. We wish to show it holds for k + 1 {\displaystyle k+1} nodes. Let u be the next visited node according to the algorithm, i.e. the node with minimum dist. We claim that dist is the shortest distance from source to u.

To prove this claim, we proceed by contradiction. If there were a shorter path, then this shorter path either contains another unvisited node or not.

For all other visited nodes v, the dist is already known to be the shortest distance from source already, because of the inductive hypothesis, and these values are unchanged.

After processing u, it will still be true that for each unvisited node w, dist will be the shortest distance from source to w using visited nodes only. If there were a shorter path that did not use u, we would have found it previously, and if there were a shorter path using u we would have updated it when processing u.

After all nodes are visited, the shortest path from source to any node v consists only of visited nodes. Therefore, dist is the shortest distance.