Exploiting Dijkstra's Invariant
Dijkstra's correctness depends on this invariant, which states that all edge weights must be non-negative real numbers and that for any given edge ,
This matters because the algorithm finalizes a node's shortest distance the moment it pops from the heap. Since extending any other possible path that reaches the same node can only add cost, no later route can beat the distance that was already found (the first time we pop this node).
Let us define this formally. A path is a collection of edges, and the sum is actually a statistic of that collection. The sum of a path can be written as
Suppose has just been popped from the heap. Consider any later route that reaches through some node and a final edge . Since Dijkstra pops nodes in non-decreasing distance order,
and by assumption,
Therefore,
The above equation only holds because weights are non-negative. So the sum can only stay the same or increase when a new edge is added. Formally, if a path is extended by an edge , then
It applies not only to the sum but also to other stats. For example, the maximum edge weight seen on a path is
and after extending the path,
Extending a path can introduce a larger edge weight, but it can never remove the largest edge weight that was already present. This is the statistic used in Swim in Rising Water.
The common observation is that both the sum statistic and the max statistic are monotonically nondecreasing under path extension.
This means that as long as the property under consideration has this same behavior, a Dijkstra-style approach can be correct.