Loop invariant

루프 불변성
Initialization : 첫 루프를 시작하기 전에 참이다.
Maintenance : 루프 돌기 전에 참이라면 다음 루프때에도 참이다.
Termination : 루프가 종료 되었을때 루프불변성이 알고리즘의 정당성을 증명하는데 유용한 성질을 가져야 한다.


예 )  Insertion sort (삽입정렬)

int a[10] = {0,5,2,7,10,22,1,6,8,55};
for(int j=1;j<10;++j){
    int k = a[j];
    int i = j-1;
    while(i>=0 && a[i]>k){
        a[i+1] = a[i];
        --i;
    }
    a[i+1] = k;
}

Initialization : 첫 루프를 시작하기전에 a[0] (j보다 작은) 은 오름차순으로 정렬 된 상태이다.

Maintenance : j일때 a[0 ~ j-1]이 오름차순으로 정렬된 상태라고 하자. 내부에 while문은 i<0 이거나 a[i]<=k 일때 빠져나오게 된다. 만약 i<0 이라면 이는 k가 a[0~j]중에서 제일 작다는 뜻이고 a[0]에 k를 넣으면 다음 루프에서 j+1 일때 a[0 ~ j]가 오름차순으로 정렬된 상태가 되므로 보존성을 지킨다.

만약 a[i]<=k 이기 때문에 while문을 빠져 나왔다면 k는 a[i+1]의 위치에 들어가면 다음루프에서 j+1 일때 a[0 ~ j]가 오름차순으로 정렬된 상태이므로 마찬가지로 보존성을 지킨다.

Termination : j가 10(배열의 크기)가 되어 for 루프를 빠져나왔을때 위에서 보였듯이 a[0~9(j-1)]은 오름차순으로 정렬된 상태일 것이다. 따라서 위 삽입정렬의 알고리즘은 올바르다.