루프 불변성
루프 불변성은 루프의 가능한 모든 각 반복마다 항상 성립하는 알고리즘의 특성또는 조건이다.
루프 불변성(Termination을 포함한)을 통해 알고리즘의 타당성, 정확성을 입증할 수 있다.
루프 불변성이 성립하려면, 다음 조건들을 만족해야 한다.
루프 불변성의 조건
- 초기 조건 : 루프가 첫 번째 반복을 시작하기 전 루프 불변성이 성립
- 유지 조건 : 루프의 반복이 시작되기 전 루프 불변성이 참이었다면 다음 반복 시작 전까지도 계속 성립
- 종료 조건 : 루프가 종료될 때 발생하는 상태가 알고리즘의 타당성을 보이는 데 도움이 되는 유용한 특성을 가짐
알고리즘의 타당성 증명 순서
- 루프 시작 전에 루프 불변성이 성립함을 보인다.
- 어떤 반복을 시작할 때(j번째 iteration) 루프 불변성이 성립한다고 가정한다.
- 다음 반복을 시작할 때(j+1번째 iteration) 루프 불변성이 성립함을 보인다.
- 루프가 종료될 때의 상태를 보이고, 유용한 결과를 얻었음을 보인다.
삽입정렬의 예
INSERTON-SORT(A)
1 for j = 2 to A.length
2 key = A[j]
3 i = j - 1
5 while i > 0 and A[i] > key
6 A[i+1] = A[i] // key의 위치를 찾을 때 까지 원소를 이동
7 i = i-1
8 A[i+1] = key루프 불변성 : j번째 루프시작 전, A[1..j-1]은 정렬되어 있다.
초기 조건
j=2일 때, 배열 A[1..1]는 하나의 값만 있으므로 정렬되어 있다.
유지 조건
루프가 j번째 반복시작 전, A[1..j-1]은 정렬되어 있다고 가정한다.
루프의 while문에서 올바르게 정렬되는 key의 적절한 위치를 찾을 때까지 배열을 오른쪽으로 이동시킨다. 적절한 위치에 key를 삽입하고 j를 1증가시키면 A[1..j]가 정렬되어 있고, j+1번째 반복을 시작할 때 루프 불변성이 성립한다.
종료 조건
j=A.length+1, i=A.length일 때 루프가 종료되며 A[1..A.length]가 정렬되었다.
따라서 루프 불변성이 성립하며, 알고리즘이 타당하다.
