Review of loop invariants

Insertion Sort – review of loop invariants

Insertion Sort

• Problem: sort n numbers in A[1..n].

• Input: n, numbers in A

• Output: A in sorted order:  i  [2..n], A[i-1] <= A[i]

Loop Invariants

• Invariants – statements about an algorithm that remain valid

• We must show three things about loop invariants:

• Initialization – statement is true before first iteration
• Maintenance – if it is true before an iteration, then it remains true before the next iteration
• Termination – when loop terminates the invariant gives a useful property to show the correctness of the algorithm

Example: Insertion Sort

• Invariant: at the start of each for loop, A[1…j-1] consists of elements originally in A[1…j-1] but in sorted order

Example: Insertion Sort

• Invariant: at the start of each for loop, A[1…j-1] consists of elements originally in A[1…j-1] but in sorted order

Example: Insertion Sort

• Invariant: at the start of each for loop, A[1…j-1] consists of elements originally in A[1…j-1] but in sorted order

Example: Insertion Sort

• Invariant: at the start of each for loop, A[1…j-1] consists of elements originally in A[1…j-1] but in sorted order