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

2

6

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!

Pygmy answered 9/11, 2016 at 3:23 Comment(0)
B
6

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.

Boatsman answered 18/11, 2016 at 6:41 Comment(0)
M
0
  • Before the merge occurs, Merge-sort divides the array into subarrays until it breaks it down into single index arrays. These single index arrays are considered "sorted"/ordered (Initialization).

  • Prior to calling merge, the subarrays are ordered (Initialization cont.).

  • As the merge is happening, the subarrays that are being merged during the merge loops are ordered (Maintenance).

  • Once the loops are finished, the subarray continues to be ordered (termination).

This remains true as the merge-sort function continues to execute its recursive calls and merges more and more ordered subarrays until you have completed the function, and all recursion calls have been executed.

Matthiew answered 2/9 at 15:50 Comment(1)
The original and almost all actual library implementations of merge sort are a hybrid of insertion sort and iterative bottom up merge sort. Top down merge sort is mostly used for academic purposes.Angelitaangell

© 2022 - 2024 — McMap. All rights reserved.