루프 불변성은 알고리즘이 타당한 이유를 쉽게 이해할 수 있도록 하기 위해서 사용된다.
루프 불변성을 보이기 위해서 세 가지 특성인 초기조건, 유지조건, 종료조건을 모두 만족해야 한다.
- 초기조건: 루프가 첫 번째 반복을 시작하기 전에 루프 불변성이 참이어야 한다.
- 유지조건: 루프의 반복이 시작되기 전에 루프 불변성이 참이었다면 다음 반복이 시작되기 전까지도 계속 참이어야 한다.
- 종료조건: 루프가 종료될 때 그 불변식이 알고리즘의 타당성을 보이는 데 도움이 될 유용한 특성을 가져야 한다.
초기조건과 유지조건을 만족하면 루프가 반복을 시작하는 순간에 루프 불변성은 항상 참이다. 첫 반복이 시작되기 전에 불변식을 만족함을 보이고, 다음 반복으로 넘어갈 때 불변식이 만족함을 보이는 것은 수학적 귀납법과 유사하다.
※ 수학적 귀납법이란?
- P(0)이 성립한다.
- 임의의 $n \in N$에 대하여, $P(n)$이 성립한다면, $P(n+1)$ 역시 성립한다.(여기서, $N$은 자연수 집합)
그렇다면, 임의의 $n \in N$에 대하여, $P(n)$이 성립한다. 이것을 수학적 귀납법이라고 한다.
종료조건이 가장 중요한데, 이는 루프 불변성을 보이는 목적이 결국 알고리즘의 타당성을 보이는 것이기 때문이다.
보통 루프의 종료조건이 완료될 때까지 루프 불변성을 이용한다. 일반적인 수학적 귀납법은 귀납적 과정이 무한히 반복되는 데 반해 여기서는 루프가 종료될 때 귀납적 과정도 끝난다.
루프 불변성의 개념을 삽입 정렬에 적용시켜서 삽입 정렬 알고리즘이 타당함을 보이려고 한다.
아래의 의사코드는 정렬된 배열 $A[1, ..., j-1]$에 새로운 값인 $A[j]$를 삽입하는 삽입정렬의 의사코드이다.
INSERTION-SORT(A)
for j=2 to A.length
key = A[j]
// A[j]를 정렬된 배열 A[1, ..., j-1]에 삽입한다.
i = j - 1
while i>0 and A[i] > key
A[i+1] = A[i]
i = i - 1
A[i+1] = key
- 초기조건: 루프의 첫 반복이 시작하는 시점인 $j=2$일 때 루프 불변성이 성립하는지 살펴본다. 시작하는 경우 부분배열 A[1 ... j-1]은 A[1] 한 개의 원소로 구성되어 있으므로 정렬되어 있으므로, 루프의 첫 반복 시작 전에 루프 불변성이 만족한다.
- 유지조건: 매 반복 시 루프 불변성이 유지되는지를 살펴본다. 삽입 정렬에서는 A[j]가 올바른 위치를 찾을 때까지 기존의 부분 배열을 오른쪽으로 한 칸씩 이동시키면서 적절한 위치에 삽입된다. 따라서 매 반복시 부분 배열인 A[1 ... j]는 정렬된 상태로 유지된다. 따라서 루프 불변성이 유지된다.
- 종료조건: 루프가 종료 되었을 때 어떤 상황이 발생하는지 조사해본다. 삽입 정렬의 경우에는 전체 배열인 A[1 ... n]이 정렬되었으면 알고리즘이 타당함을 의미한다.