A loop invariant is a property of a loop that holds True:
- Before the loop (Initialization)
- After each iteration of the loop (Maintenance)
- After the loop (Termination)
However, a loop invariant does not necessarily have to be true throughout the loop.
A loop invariant can be used in a inductive proof to prove an algorithm is correct
Proof by induction using loop invariants
To prove an algorithm’s correctness using loop invariants, we must show:
- The loop invariant is True before the start of the first loop.
- If the loop invariant is True for one iteration of the loop, then it is True for the next iteration.
- When the loop terminates, the loop invariant, along with the reason that the loop terminated, gives us a useful property.
Note that the loop invariant isn’t necessarily True throughout the loop.
Prim’s Algorithm
Proof Of Correctness
Via Loop Invariants
Loop Invariant: The subtree T generated by Prim’s is a subset of the true MST (T*) for all iterations
Initialization: Before the loop, T contains no edges. Therefore, it can be trivially proven that T is a subset of T*, as an empty set is a subset of all sets:
Maintenance: For each iteration, Prim’s only selects the cheapest edge, , and does not permit it to cause an cycles. According to the cut property, all MSTs contain e, therefore
Termination: The loop terminates only when all the nodes from T* are in T. Since, for each iteration, T is a subset of T*, during the termination of loop T = T*.
Link to source