# Merge Sort
## pseudocode

void mergeSort(A , p , r)
    if p + 1 < r:
        q = (p + r) / 2
        mergeSort(A , p , q)
        mergeSort(A , q , r)
        merge(A , p , q , r)

void merge(A , p , q , r){
    len1 = q - p
    len2 = r - q
    把A[p] ~ A[q - 1]依序複製到新陣列arrL
    把A[q] ~ A[r - 1]依序複製到新陣列arrR
    arrL[len1] = oo
    arrR[len2] = oo
    i = 0 , j = 0
    for k = p to r - 1:
        if arrL[i] <= arrR[j]:
            A[k] = arrL[i]
            i++
        else:
            A[k] = arrR[j]
            j++
}

## loop invariant
見merge函式，設:
一、 arrL[i]:arrL中還沒放進A陣列的最小值(arrL[0]~arrL[i - 1]已經放進A了)
二、 arrR[j]:arrR中還沒放進A陣列的最小值(arrR[0]~arrR[j - 1]已經放進A了)
三、 A[p] ~ A[k - 1]為前k - q小(arrL與arrR中)的值，並且排序好放在A中

1. **initialization**: i = 0 , j = 0，代表此時arrL與arrR都還沒放數值進A，因此k = p，A[p] ~ A[p - 1]中沒有數值，成立。
2. **maintenance**: 現在有i,j,k三個位置，以上三個假設會先成立，那現在要證明迴圈內的code執行一次後，三個假設仍然會成立。因為假設先成立了，A[p] ~ A[k - 1]是前k - q小的值，設現在是arrL[i] <= arrR[j]，arrL[i]會是arrL[i] ~ arrL[len1]與arrR[j] ~ arrR[len2]中的最小值，這個最小值放到A[k]後，第三條假設會成立(在k++後)，再來i++後，第一條假設也會成立，而j沒有動，所以第二條假設也會成立，因此，回圈內的code執行一次後，三個假設仍然會成立。(如果是arrL[i] > arrR[j]假設也會成立，證明方法跟上面的一樣)
3. **termination**: 當k = r，A[p] ~ A[r - 1]為前r - q小(arrL與arrR中)的值，並且排序好放在A中(即為所求)，也就是說，除了arrL[len1]與arrR[len2]這兩個無限大以外，arrL與arrR中所有的值都會放在A[p] ~ A[r - 1]中，因為i會停在len1，j會停在len2，根據假設，arrL[i]與arrR[j]不會被放進A中。

## recurion的正確性
見mergeSort，函式定義是把A[p] ~ A[r - 1]由小到大排序，當r = p + 1時，A[p] ~ A[p]只有一個元素，不用排序，所以一個元素的情況是合法的；當r < p + 1時，A[p] ~ A[r - 1]根本沒有元素，也不用排序，因此只有當p + 1 < r時，才要sort，所以沒有元素的情況是合法的。
再來討論p + 1 < r的情況，當p + 2 == r時，也就是A有兩個元素的情況，q會切在中間，把A一分為二，左右各一個元素，而一個元素的情況是合法的(上面有處理)，所以兩個元素的情況也是合法的；當p + 3 == r時，也就是A有三個元素的情況，q會切在靠左的位置，左邊有一個元素，右邊有兩個元素，一個元素與兩個元素都是合法的，所以三個元素的情況也是合法的，以此類推，mergeSort函式可以處理各種數量，它不會有無窮recursion的情況。