Prev: Programming Using Induction Next: Invariants and Recursive Algorithms 
What Every CMPT 225 Student Should Know About Mathematical Induction
 by Brad Bart, Simon Fraser University  
Part 1: Overview of Induction
Part 2: How Induction Relates to Computer Science

Part 2: How Induction Relates to Computer Science
Loop Invariants  
The loop invariants for the iterative SumOdd(n)
look very much like the
inductive step. This is not a coincidence. Loop invariants are
usually statements about an algorithm that you can prove by
induction. The most useful invariants will be about either:
A[0..n1] :
void isort(int *A, int n) { for (int i = 1; i < n; i++) { // insert A[i] into A[0..i1] int temp = A[i]; int j = i1; // shift all A[] > temp while (j >= 0 && A[j] > temp) { A[j+1] = A[j]; j; } A[j+1] = temp; } } 
Iterative SumOdd :
int SumOdd(int n) { total = 1; for (int i = 2; i <= n; ++i) { assert(total == (i1)*(i1)); total += (2*i  1); assert(total == i*i); } }  
Demo of Insertion Sort:

To explain the algorithm, the correct position of A[i] is
located by finding all those elements to its left which are larger.
Those elements are shifted up by one position to make
space for the insertion of A[i] . A demonstration on
an array of 7 elements is shown to the
left.
Insertion Sort is an incremental sort.
Each loop begins with a sorted At the beginning of each loop,This is a loop invariant about the progress of the algorithm. Once you have declared a loop invariant, your next goal is to prove it by induction. Why? Because the byproduct of your proof will be a proof of correctness of the algorithm.
Remember that the goal of a sorting algorithm is to permute
the elements of  
Proof (by induction on i ):
 ^{1}A more formal treatment would verify these properties of the inner while loop, probably by stating (and proving) a separate loop invariant.  
And now to declare an invariant about the running time. Because the inner while loop runs an indefinite number of times, it will be impossible to construct an invariant that states the running time as an equation. Instead, the loop invariant will be a description of the worst case, i.e., the largest number of steps, using an inequality.  
void isort(int *A, int n) { for (int i = 1; i < n; i++) { // insert A[i] into A[0..i1] int temp = A[i]; int j = i1; // shift all A[] > temp while (j >= 0 && A[j] > temp) { A[j+1] = A[j]; j; } A[j+1] = temp; } } 
On each iteration of the while loop, there are
2 comparisons for testing the entry condition and
2 assignment operations for shifting
Each iteration of the outer for loop performs
3 assignment operations plus at most
4i + 1
operations for the inner
while, so the running time of the
The total running time, T(k), of the loops i = 1, . . ., k, satisfies: . Proof (by induction on k):
. . . and this proves that Insertion Sort runs in quadratic time in the worst case.  
Next: Invariants and Recursive Algorithms 