정렬 정당성 증명

loop invariant를 이용한 정렬 알고리즘 정당성 증명

 

삽입 정렬

초기: arr[:1]은 정렬 되어 있다

유지: loop가 끝나면 arr[:i] 정렬되어있다.

종료: arr 정렬되어있다

 

버블 정렬

초기: arr[n-1:n] 정렬되어있다

유지: loop 끝나면 arr[i:n] 정렬되어있다

종료: arr 정렬

 

3273 두 수의 합

투포인터 정당성 증명

배열 arr이 정렬된 상태

    int s = 0, e = n-1;
    for (int i = 0; i < n; i++) {
        if (s==e) break;
        int tmp = arr[s]+arr[e];
        if (tmp<x) s++;
        else if (tmp>x) e--;
        else {
            ans++;
            e--;
        }
    }

a[i] < a[j], i<j 일때

유지 조건

arr[i]+arr[j](앞으로는 이를 tmp라 명명) > x 이면, j보다 큰 구간에서 모든 경우 tmp의 값은 > x임으로 j--

tmp < x 이면, i보다 작은 모든 구간에서 가능한 tmp의 값은 < x임으로 i++

즉 arr[i:j] 범위 밖에서 가능한 모든 경우를 탐색하고 구간 i~j를 줄여가고 i~j 구간이 0이 되는 순간 종료