use entirely array-based priority queues without decrease-key functionality, which have been found to achieve even faster computing times in practice. However, the difference in performance was found to be narrower for denser graphs. Proof of correctness Proof of Dijkstra's algorithm is constructed by induction on the number of visited nodes. Invariant hypothesis: For each visited node , is the shortest distance from to , and for each unvisited node , is the shortest distance from to when traveling via visited nodes only, or infinity if no such path exists. (Note: we do not assume is the actual shortest distance for unvisited nodes, while is the actual shortest distance) The base case is when there is just one visited node, namely the initial node , in which case the hypothesis is trivial. Next, assume the hypothesis for k-1 visited nodes. Next, we choose to be the next visited node according to the algorithm. We claim that is the shortest distance from to . To prove that claim, we will proceed with a proof by contradiction. If there were a shorter path, then there can be two cases, either the shortest path contains another unvisited node or not. In the first case, let be the first unvisited node on the shortest path. By the induction hypothesis, the shortest path from to and through visited node only has cost and respectively. That means the cost of going from to through has the cost of at least + the minimal cost of going from to . As the edge costs are positive, the minimal cost of going from to is a positive number. Also < because the algorithm picked instead of . Now we arrived at a contradiction that < yet + a positive number < . In the second case, let be the last but one node on the shortest path. That means . That is a contradiction because by the time is visited, it should have set to at most . For all other visited nodes , the induction hypothesis told us is the shortest distance from already, and the algorithm step is not changing that. After processing it will still be true that for each unvisited node , will be the shortest distance from to using visited nodes only, because if there were a shorter path that doesn't go by we would have found it previously, and if there were a