Using Loop invariant to prove correctness of merge sort (Initialization , Maintenance , Termination)

Question

How would you go about proving the correctness of merge sort with reasoning over the states of loop invariants?.The only thing that i can visualize is that during the merge step the subarrays(invariants) when combined maintain their states i-e they are again sorted at each merge step.But i don't know if i am proceeding correctly or not.I don't have much understanding of Loop invariants and stuff.Can some one enlighten me on this one ?. Explain what will happen at each phase

a) Initialization b) Maintenance c) Termination

Much obliged!

Solution

pseudocode for Merge sort

MERGE-SORT(A, p, r)

    1 if p < r
    2    then q <-- [(p + r) / 2]
    3          MERGE-SORT(A, p, q)
    4          MERGE-SORT(A, q + 1, r)
    5          MERGE-SORT(A, p, q, r)

MERGE-SORT(A, p, q, r)

    1  n1 <-- q - p + 1 
    2  n2 <-- r - q
    3  create arrays L[1 ... n1 + 1] and R[1 ... n2 + 1]
    4  for i <-- 1 to n1
    5       do L[i] <-- A[p + i - 1]
    6  for j <-- 1 to n2
    7      do R[j] <-- A[q + j]
    8  L[n1 + 1] <-- infinite 
    9  R[n2 + 1] <-- infinite
    10 i <-- 1
    11 j <-- 1
    12 for k <-- p to r
    13     do if L[i] <= R[j]
    14           then A[k] <-- L[i]
    15                i <-- i + 1
    16           else A[k] <-- R[j]
    17                j <-- j + 1

We try to sort two piles of cards but we avoid checking whether either pile is empty in each basic step, and we use the infinite as a sentinel card to simplify our code. So, whenever the sentinel card infinie is exposed, it cannot be the smaller card unless both piles have their sentinel card exposed. But once that happens, all the non-sentinel cards have already been placed onto the output pile. Since we know in advance that exactly r - p + 1 cards will be placed onto the output pile, we can stop once we have performed that many basic steps.

• Loop Invariant:

  • Initialization: prior to the first iteration of the loop, we have k = p, so that subarray A[p ... k - 1] is empty. this empty subarray contains the k - p = 0 smallest elements of L and R, and since i = j = 1, both L[i] and R[j] are the smallest elements of their arrays that have not been copied back into A.

  • Maintenance: To see that each iteration maintains the loop invariant, let us first suppose that l[i] <= R[j]. Then L[i] is the smallest element not yet copied back into A. Because A[p ... k - 1] contains the k - p smallest elements, after line 14 copies L[i] into A[k], the subarray A[p ... k] will contain the k - p + 1 smallest elements. Incrementing k(in the for loop update) and i(in line 15) re-establishes the loop invariant for the next iteration. If instead L[i] > R[j], then lines 16-17 perform the appropriate action to maintain the loop invariant.

  • Termination: At termination, k = r + 1. By the loop invariant, the subarray A[p ... k - 1], which is A[p ... r], contains the k - p = r - p + 1 smallest elements of L[1 ... n1 + 1] and R[1 ... n2 + 1], in sorted order. The arrays L and R together contain n1 + n2 + 2 = r - p + 3 elements. All but the two largest elements have been copied back into A, and these two largest elements are the sentinels.