[알고리즘/이론]루프 불변성(Loop Invariant) - 알고리즘의 타당성을 증명하기 위해..

루프 불변성은 알고리즘이 타당한지 확인하기 위해 사용되는 성질 중 하나이다.

쉽게 설명하자면 우리가 작성한 알고리즘 내부에 for나 while 같이 반복문이 삽입되어 있을 때 그것이 원하는 결과를 출력하는지 루프 불변성을 통해 확인하는 것이다.

 

루프 불변성을 통해 알고리즘의 타당성을 증명하기 위해 만족시켜야 하는 3가지 조건들이 있다.

1.  루프가 첫 번째 반복을 시작하기 전에 루프 불변성이 유지되어야 한다.

2.  루프가 반복되기 전에 루프 불변성이 유지되었다면 다음 반복이 시작되기 전까지도 계속 유지되어야 한다.

- 위의 2가지만 만족시키더라도 루프 불변성이 유지됨을 알 수 있다.

3.  루프가 종료될 때 유지된 루프 불변성이 알고리즘 타당성 증명에 의미가 있어야 한다.

- 확인한 루프 불변성을 알고리즘 타당성 증명에 사용하기 위해서는 3번 또한 만족시켜야 하며 어떻게 보면 가장 중요한 부분이라고 할 수 있다.

 

언뜻 보면 무언가 비슷한 것을 배운 적이 있다. 바로 수학적 귀납법이다.

기저 명제 + 귀납적 과정을 통해 임의의 수에 대한 명제가 참일을 보이는 증명 방법이다. 

차이라고 할만한 점은 알고리즘의 경우에는 언젠가는 종료된다는 것이다.

.