Question 5.3

Proof of Correctness of Merge: Loop invariant (of the first while loop): At the start of each iteration, array[left … k] contains the (k - left) smallest elements of arr1 and arr2 in sorted order. Also, at the start of each iteration, the variable “count” stores the number of possible transposition pairs between elements from arr1[i … length_arr1 - 1] and elements from arr2[0 … j-1]. Initialization: At the beginning, k is left, so array[left … k] is just one element, which is already sorted. Also, there must not be a transposition pair formed by only one element, so count is 0. Invariant holds. Maintenance: Assume variant holds for kth iteration, and array[i] < array[j], then array[i] is the smallest among elements not yet copied to C. Also, it means that arr1[i] (in the left array) is already smaller or equal than all elements in array[j … arr2.length - 1], so no need to increase “count”. Therefore, the invariant holds in the next iteration. Assume variant holds for kth iteration, and array[i] > array[j], then array[j] is the smallest among elements not yet copied to C. Also, it means that arr2[j] (in the right array) is smaller than all elements in arr1[i … length_arr1-1], so we need to increase “count” by the amount of (length_arr1 - i) since there are this many transpositions pair could be formed from array[j] and from all elements in array[i … length_arr1]. Therefore, the invariant holds in the next iteration. Termination: When i = length_arr1 or j = length_arr2, loop ends and the elements in array[left … k] are already sorted (after the remaining two while loops, array[left … right] will be sorted). Also, the variable “count” stores the number of possible transposition pairs between elements from array[left … right]. Proof of correctness of mergesort: follows merge.