Insertion Sort

The Insertion Sort from the text. Note that the text's algorithm arrays are based at 1, Java and C++ arrays are based at 0.

Example

• The array to the left of the dark element is always sorted ascending order.
   
• The dark element is inserted into the sorted array.
   
• Sorted order maintained by shifting larger sorted elements to the right one position, as in (d) and (e).

Figures a-e: immediately after assignment to j (i.e. darkened)

1. j=2, A[1..1] is sorted
2. j=3, A[1..2] is sorted
3. j=4, A[1..3] is sorted
4. j=5, A[1..4] is sorted
5. j=6, A[1..5] is sorted
6. j=7, A[1..6] is sorted

Two nested loops are required:

1. Outer loop iterates over all elements of the array,
    
2. Inner loop shifts larger sorted elements to right.

Pre and Postconditions

• pre - method parameter A != null
   
• post - \forall int i; 0 <= i && i < A.length-1 && A.length > 1; A[i] <= A[i+1]

          States that array A[0..A.length-1] is sorted in ascending order and array has at least 2 elements.

Initialization, Maintenance and Termination

Outer loop - iterate over each array element

• loop_invariant (\forall int k; k>=0 && k <= j-1; A[k] <= A[j-1]);

       for( j=1; j<A.length; j++) {

  Initialization: Prior to first iteration of for statement: A[0..0] <= A[0]; A[0] maximum of A[0..0].

  Maintenance: At start and end of each iteration of for statement: A[0..j-1] <= A[j-1]; A[j-1] maximum of A[0..j-1].

  Termination: j=A.length, by loop invariant A[0..j-1] <= A[j-1]; A[j-1] maximum of A[0..j-1].

  Inner loop - shifts larger sorted elements to right
   

• loop_invariant (\forall int k; k>=0 && k < i; A[k] <= A[k+1]);
  
       while (i > -1 && A[i] > key) {

  Initialization: Prior to first iteration of while statement: A[0..i]  is sorted. When i=0, range of k, k>=0 && k < 0, is empty so is sorted.

  Maintenance: At start and end of each iteration of while statement: A[0..i] is sorted.

  Termination: Each iteration i=i-1, until i=-1. A[0..-1] is empty hence sorted.

  Note that in (d) at loop termination

  A = {2, 2, 4, 5, 6, 3 }

  i = -1

  key = 1

  A[i+1] = key

  A = {1, 2, 4, 5, 6, 3 }

  

Note: arrays start at index 0.

class InsertionSort { //@ pre A != null; //@ modifies A[*]; //@ post (\forall int i; 0 <= i && i < A.length-1; A[i] <= A[i+1]);   void insertionsort(int A[]) {         int i, j, key;         //@ loop_invariant (\forall int k; k>=0 && k <= j-1; A[k] <= A[j-1]);         for( j=1; j<A.length; j++) {             key = A[j];             i = j - 1;            //@ loop_invariant (\forall int k; k>=0 && k < i; A[k] <= A[k+1]);            while (i > -1 && A[i] > key) {                  A[i+1] = A[i];                                 // Shift right values > key                  i = i - 1;             }             A[i+1] = key;        }    } }

Question 2.10

1. What does the postcondition mean?

   //@ post (\forall int i; 0 <= i && i < A.length-1; A[i] <= A[i+1]);

2. What does the following loop-invariant of the outer loop, for mean?

   //@ loop_invariant (\forall int k; k>=0 && k <= j-1; A[k] <= A[j-1]);

   Is that what we want? Does that correspond to the code? This is tricky.
    

3. What is implied by changing the loop-invariant of the for to:

   //@ loop_invariant (\forall int k; k>=0 && k < j-1; A[k] <= A[k+1]);

   Does that correspond to the code?
    

4. What is implied by changing the loop-invariant of the for to:

   //@ loop_invariant (\forall int k; k>=0 && k < j-1; A[k] >= A[k+1]);