Loop Invariant
A loop-invariant proof is a proof based on the principles of mathematical induction that proves the correctness of an algorithm using a property or condition that holds true before and after each iteration of a loop throughout its execution, called a loop invariant. A loop-invariant proof consists of the following steps:
Initialization: Proving that the loop invariant is true before the execution of the loop (Base Case).
Maintenance: Assuming that the loop invariant is true before an iteration of the loop (Inductive Hypothesis), and proving that it remains true after the iteration (Inductive Step).
Termination: Proving that when the loop terminates, the invariant, combined with the termination condition, implies the correctness of the algorithm.
Finiteness
Since all loops are finite, we must make a distinction between induction and loop-invariant proofs. This also suggests that although step two shows that the loop invariant must hold true after the iteration, it does not necessarily need to