int sort(int a[], int n)
{
    int i, j, m;
    for(i=0; i<n; i++) {
        // find minimum
        m = i;
        for (j=i; j<n; j++)
            if (a[m] > a[j]) m = j;
        swap(a[i], a[m]);
    }
    return;
}

• 구분을 위해, Sorting이 끝난 후 배열에 저장된 값들을 b[0], b[1], …,b[n-1]라고 부르자
• 조건 1: {a[0], a[1], …, a[n-1]} = {b[0], b[1], …, b[n-1]}. 두 집합이 같음 (없어지거나 새로 생기는 값이 없어야 함)
• 조건 2: b[0] < b[1] < … < b[n-1] (편의상 같은 값은 없다고 가정)

• 배열 요소를 교환만 하므로, 집합 조건을 깰 수 있는 코드는 없음
• Invariant: k번째 루프가 끝난 후에

2. a[k-1] < a[x] if x > k-1

• 이제 수학적 귀납법을 통해 invariant를 증명하자
• Base : k = 0
• 1. a[0]부터 a[-1]까지? 성립하는지 확인할 조건 자체가 없으므로(null condition) true가 된다.
• 2. a[-1]은 말이 안 됨. null condition 이므로 true.
• Step : k번째 루프가 끝났을 때 Invariant가 성립한다면, k+1번째 루프가 끝났을 때도 Invariant가 성립하는가?

• a[k] < a[x] if x > k

int sort(int a[], int n)
{
    if (n<=1) return;
    int j, m;
    m = 0;
    for(j=0; j<n; j++) {
        if (a[m] > a[j]) m = j;
    }
    swap(a[0], a[m]);
    sort(a+1, n-1);
    return;
}

• Base : n = 1일 때, 할 일이 없음.
• Step : n-1일 때 sort() 함수가 성공한다면 (즉, 재귀 호출이 끝난 후 a[1]<a[2]<…<a[n-1] 이라면), n일 때 sort() 함수가 성공하는가? (함수가 끝날 때 a[0]<a[1]<…<a[n-1]이 성립하는가?)

• 재귀호출 전 : 최소값을 a[0]에 저장하므로 a[0]<a[1], a[0]<a[2], …, a[0]<a[n-1]이 성립한다.
• 재귀호출 이후 : 가정에 따라, a[1]<a[2]<…<a[n-1]이 성립한다. 최소값을 a[0]에 저장했으므로, a[0]<a[1]이다. 따라서 n일 때 sort()함수가 성공한다.

int sort(int a[], int n)
{
    if(n==1) return;

    int h;
    h = n / 2;

    int b[n];
    copy a[] to b[];

    sort(b, h);
    sort(b+h, n-h);
    b의 두 부분을 a에 Merge;

    return;
}

• 집합 조건을 깰 수 있는 코드는 없음
• Base : n=1 → 이미 정렬이 완료된 상태. 할 일이 없음
• Step : n/2일 때 sort()함수가 성공한다면
• 즉, 재귀 호출이 끝난 후 b[0]<b[1]<...<b[h-1],  b[h]<b[h+1]<...<b[n-1] 가 성립한다면
  
• Merge 알고리즘이 성공적으로 실행될 조건이 만족되었다.
• 따라서 sort(a, n)함수가 끝날 때 a[0]<a[1]<...<a[n-1] 이 성립한다.
• 단, Merge 알고리즘의 정확성은 따로 증명해야 한다.