Loop-Invariant in Iteration
Loop Invariant(루프 불변량)은 프로그램 루프에서 모든 반복 시의 전후로 변하지 않는 성질을 의미한다.
이것은 반복문의 내용이 실행될 수록 원하는 결과값을 도출하는 과정을 이탈하지 않음을 보이는 특성이다.
j = 10
for i in range(0, 10):
j-=1위와 같은 코드에서, loop 중에는 'i+j=10' 이라는 성질은 불변하고, 이것을 loop-invariant라고 볼 수 있다.
loop-invariant는 코드가 작동하는 원리를 설명하는 특성이고, 이것이 명확하게 드러나지 않는다면 협업 시 다른 프로그래머가 이해할 수 있도록 도울 수 있는 코드를 작성해야 한다.
이것은 또한 변수간의 긴밀한 관계(루프 시 변하지 않는 성질)를 가지고 있는 iterative(반복) 알고리즘을 설계하는 데에 핵심적인 역할을 한다.
(좋은) loop invariant는 세 가지 조건을 만족해야 한다.
- Initialization: 루프의 첫 시행 이전에 반드시 초기화되어야 한다
- Maintenance: 만약 루프의 시행 이전에 invaritent가 참이라면 루프 시행 이후에도 반드시 참이어야 한다(반복문의 내용이 loop invariant를 깨뜨리지 않아야 한다)
- Termination: 루프가 종료될 때, invarient를 통해 유의미한 output 혹은 알고리즘을 이해하는데 도움이 되는 정보를 얻을 수 있어야 한다. Loop invarient가 성립하면 항상 정답을 도출했음이 증명된다.
loop invarient를 이용해서 반복문의 정당성을 증명할 수 있는데, 위의 세 가지 조건을 만족하는지 귀납법과 유사하게 증명해주면 된다.
이러한 loop-invarient는 다양한 기본 알고리즘에 적용된다.
1. Bubble Sort - 매 stage(i번째) 후에 Array에서 i번째로 큰 값은 언제나 Array의 n-1-i번째에 위치하게 된다.
2. Selection Sort - 재귀를 이용한 selection sort 구현 시 함수 단위의 execution이 종료될 때 마다 sorted array 상에서의 element의 위치가 결정된다
3. Insertion Sort - 매 stage(i번째) 후에 Array의 [0, i]의 subarray는 sorted array가 된다.
4. Binary Search - mid값은 항상 start 이상, end 이하이다. + 추가적인 불변량 조건을 통해 원하는 값이 어느 위치에 저장되어 있는지 알아낼 수 있다.