Prerequisites for the Theorem

Loop Invariant

In our algorithms, our loops finish in finite steps: hence, to check the correctness of an algorithm, we at times make use of a technique called loop invariant.

Loop invariant is a statement, that holds true at the start of each iteration of the loop.

For example, in particular, in present 1MSc, it is never-changing that at the start of each class, I will remember that Neels slept in my last class. 😉

On a serious note, we cannot just make an assertion, we need to prove that our claim that this particular “loop invariant” we found holds true in each execution. For that, we use a particular technique, similar to that of induction proofs we see in mathematics. We will first prove that the proposed loop invariant is true before the loop starts executing (After Initialization). Then we will use some techniques to prove that the loop invariant remains true in each step after initialization, before the final step (something like induction step we take in mathematics). We wind up the discussion claiming that the loop invariant remains true even when the loop terminates.

We will prove the correctness of Dijkstra’s Algorithm using a loop invariant.

Upper Bound Property

Statement: (Before Chapter outline in Chapter 24) We always have v.d ≥ 𝛿(s,v) for all vertices v ∈ V , and once v.d achieves the value 𝛿(s,v), it never changes.

The author lays two claims here:

1. v.d ≥ 𝛿(s,v) for all vertices v ∈ V
2. Once v.d achieves the value 𝛿(s,v), it never changes

We will not concern ourselves with the proof of these two claims; it is rather intuitive: v.d is path weight of some path from s to v and definitely that weight will be the least path weight among any path between s and v – hence the first claim. Since any path from s to v cannot have weight smaller than the weight of shortest path weight, the second claim is also true.

No-path property

If there is no path from s to v, then we always have u.d = 𝛿(s,u) = ∞.

Convergence Property

If s ↝ u → v is a shortest path in G for some u, v ∈ V, and if u.d = 𝛿(s,u) at any time prior to relaxing edge (u,v) then v.d = 𝛿(s,v) at all times afterward.

Proof of these properties are given in section 24.5

Pages: Contents … << Previous 7 Next Page>>