How to prove the correctness of insertion sort with recursion?

Question

I have to do insertion sort with recursion and prove its correctness by using a loop invariant. I am confident that my code is correct and it works with different inputs. But, I don't know how to prove its correctness the way my book does. Can someone prove it is correct by using a loop invariant ?

The algorithms are proved correct in the book by using the steps below which are similar to mathematical induction. If needed, refer enter link description here

1 - Find the loop invariant for each loop in your algorithm. The loop invariant is a condition which is true before the start of the loop, after any of the subsequent iterations and upon termination of the loop.

2 - Use logic to prove that the loop invariants are true prior before loop initialization, are maintained in subsequent loop runs and are true when the loop has terminated.

//n - The index till which the array D is to be sorted.
public static void sort(int n, int [] D){
    if(n == 0){
        return;
    }else {
        sort(n-1, D);
    }

    int lastItem = D[n];
    int j = n-1;

    while (j >= 0 && lastItem < D[j]) {
        D[j + 1] = D[j];
        j--;
    }

    //Insert the lastItem at the correct position.
    D[j+1] = lastItem;
}

}

PS - The book I use is "Introduction to Algorithms" by Thomas Cormen i.e. the CLRS book.

You can start by noting that this recursive form is equivalent to using a loop, and then prove the loop-based version is correct. — kaya3, Feb 11 '20 at 01:57

score 1 · Answer 1 · answered Feb 13 '20 at 20:21

The loop invariant is that after the call D[0..n] contains the first n values of the original array and for all i < n, D[i] <= D[i+1].

It is trivially true for n = 0. And after the recursive call you know by induction that it is true for n-1. The "contains the first n values of the original array"is true at all points. The conditionD[i] <= D[i+1]` will start with only one exception, but that exception moves through your loop, and you exit the loop when the exception disappears.

Have fun writing that up formally! :-)

The formal part is difficult for me. I just know that my code works. I also some tests for it. — Erran Morad, Feb 14 '20 at 18:36

Evgeniy Mironov · Answer 2 · 2020-02-20T11:18:17.573

May be answer is somewhat redundant. For convenience we split method on two parts - recursion and loop. Loop invariant is described in code below:

// Correctness of sort can be proved by mathematical induction
public static void sort(int n, int[] D)
{
    if (n == 0)
    {
        return;
    }
    else
    {
        sort(n - 1, D);
    }
    InsertNElementInSortedArray(n, D);
}

// This method insert n-th element of D in already sorted slice D[0 .. n-1] (right bound included).
// After method execution we have sorted slice D[0 .. n] (right bound included).
// Case 1. n==0. We swap 0-th element with 0-th element.
// Case 2. n > 0 and first n element sorted in D. Use loop invariant method only for this case.
// P.S. Case 1-2 can be combined.
public static void InsertNElementInSortedArray(int n, int[] D)
{
    int lastItem = D[n];
    int j = n - 1;

    // Define DR as slice of D[j+1 .. n] (right bound included)
    // Define DL as slice of D[0 .. j] (right bound included)
    // Loop invariant: DR are sorted
    //                 DL are sorted 
    //                 All elements in DR except first element are greater or equal than all elements in DL
    //                 All elements in DR except first element are greater or equal than lastItem
    //                 DR (except first element) and DL contains all elements from source D[0 .. n-1] (right bound included)
    //
    // Initialization: It is true prior to the first iteration of the loop:
    //                 DR are sorted because DR have only one element
    //                 DL are sorted because first n element sorted in D
    //                 All elements in DR except first are greater or equal than all elements in DL because DR have only one element lastItem
    //                 All elements in DR except first element are greater or equal than lastItem because DR have only one element lastItem
    //                 DR(except first element) and DL contains all elements from source D[0..n - 1] because DL == D[0..n - 1]
    //
    // Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration because
    //              In loop step we take last element from DL and replace them first element in DR and next change boundaries of DL and DR.
    //              DR are sorted because all elements in DR except first element are greater or equal than all elements in DL
    //              DL are sorted because first n element sorted in source D
    //              All elements in DR except first element are greater or equal than all elements in DL because we take maximum element from DL 
    //              All elements in DR except first element are greater or equal than lastItem because lastItem less than maximum element from DL (by loop condition)
    //              DR (except first element) and DL contains all elements from source D[0 .. n-1] by construction
    while (j >= 0 && lastItem < D[j])
    {
        D[j + 1] = D[j];
        j--;
    }

    // Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
    //              When loop terminates we have
    //              DR sorted
    //              DL sorted
    //              All elements in DR except first element are greater or equal than all elements in DL
    //              All elements in DR except first element are greater or equal than lastItem
    //              DR (except first element) and DL contains all elements from source D[0 .. n-1] (right bound included)
    //              
    //              1 case. Loop terminates when lastItem >= D[j].
    //                      lastItem is greater or equal than all elements in DL.
    //                      Replace first element from DR by lastItem. Now we have DR >= DL and both slices sorted then D[0 .. n] sorted.
    //              
    //              2 case. Loop terminates when j == -1.
    //                      DR contains all elements from source D[0 .. n-1] and DR sorted.
    //                      lastItem is less than all elements from DR.
    //                      When we assign D[0] = lastItem then then D[0 .. n] sorted.
    D[j + 1] = lastItem;
}

How to prove the correctness of insertion sort with recursion?

2 Answers2