Editing Dijkstra's algorithm (section)

== Proof ==
To prove the [[Correctness (computer science)|correctness]] of Dijkstra's algorithm, [[mathematical induction]] can be used on the number of visited nodes.<ref>{{Introduction to Algorithms|edition=4|pages=622–623|chapter=22}}</ref>

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

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

=== Induction ===
Assuming that the hypothesis holds for <math>k</math> visited nodes, to show it holds for <math>k+1</math> nodes, let {{mono|u}} be the next visited node, i.e. the node with minimum {{code|dist[u]}}. The claim is that {{code|dist[u]}} is the shortest distance from {{mono|source}} to {{mono|u}}.

The proof is by contradiction. If a shorter path were available, then this shorter path either contains another unvisited node or not.

* In the former case, let {{mono|w}} be the first unvisited node on this shorter path. By induction, the shortest paths from {{mono|source}} to {{mono|u}} and {{mono|w}} through visited nodes only have costs {{code|dist[u]}} and {{code|dist[w]}} respectively. This means the cost of going from {{mono|source}} to {{mono|u}} via {{mono|w}} has the cost of at least {{code|dist[w]}} + the minimal cost of going from {{mono|w}} to {{mono|u}}. As the edge costs are positive, the minimal cost of going from {{mono|w}} to {{mono|u}} is a positive number. However, {{code|dist[u]}} is at most {{code|dist[w]}} because otherwise w would have been picked by the priority queue instead of u. This is a contradiction, since it has already been established that {{code|dist[w]}} + a positive number < {{code|dist[u]}}.
* In the latter case, let {{mono|w}} be the last but one node on the shortest path. That means {{code|dist[w] + Graph.Edges[w,u] < dist[u]}}. That is a contradiction because by the time {{mono|w}} is visited, it should have set {{code|dist[u]}} to at most {{code|dist[w] + Graph.Edges[w,u]}}.

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

After processing {{mono|u}}, it is still true that for each unvisited node {{mono|w}}, {{code|dist[w]}} is the shortest distance from {{mono|source}} to {{mono|w}} using visited nodes only. Any shorter path that did not use {{mono|u}}, would already have been found, and if a shorter path used {{mono|u}} it would have been updated when processing {{mono|u}}.

After all nodes are visited, the shortest path from {{mono|source}} to any node {{mono|v}} consists only of visited nodes. Therefore, {{code|dist[v]}} is the shortest distance.