Question

Prove that the Merge() function of your own merge sort algorithm in the question 2 is correct using "induction on loop invariants" by following the guidelines below : (10 points)

3.1 Write down general description of loop invariant technique in your own words as proof of correctness. (2 points)

3.2 Identify the loop invariant of the loop in your merge() function (3 points)

3.3 Describe initialization step (0 points)

3.4 Describe maintenance step (4 points)

3.5 Describe Termination step (1 point)

Deliverable:

-Your answers in a simple text file format

Answer 1

3.1 Loop invariant technique:

A loop invariant is a condition that is necessarily true immediately before and immediately after each iteration of a loop.The loop invariants will be true on entry into a loop and following each iteration, so that on exit from the loop both the loop invariants and the loop termination condition can be guaranteed.

3.2 Loop Invariant

At the start of each iteration k of the for loop, the nonempty part of S contains the k − 1 smallest elements of L and R, in sorted order. Moreover, L[i] and R[j] are the smallest elements of their arrays that have not been copied to S.

3.3 Initialization Step:

The loop invariant holds prior to the first iteration of the loop. Here,i = j = 1, and S is completely empty. L[1] is the smallest element of L, while R[1] is the smallest element of R, so the initialization step holds

3.4 Maintenance Step:

Suppose without loss of generality that L[i] ≤ R[j]. Then L[i] is the smallest element not yet copied to S. The current nonempty part of S consists of the k − 1 smallest elements, so after the loop is over and L[i] is copied to S, the nonempty part of S will consist of the k smallest elements. Incrementing k (in the for loop update) and i reestablishes the loop invariant for the next iteration.

3.5 Termination Step:

At termination, k = m+ 1. By the loop invariant, S contains the m smallest elements of L and R, in sorted order. This is the result that we wanted (i.e. the merging of the two sorted arrays to produce a new sorted array).