algorithmloopssortingmergesortinvariants

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


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.