잘 모르는 개념을 인터넷에서 찾아볼때 특징들이 여러개 나열되는, 각기 다른 사이트의 설명을 보고 있노라면 개념을 명확히 알게되기 보다는 두리뭉실하게 알게된다. 마치 코끼리를 모르는 사람이 여러 목격자의 이야기를 들으면 더 묘해지는것 처럼 말이다.

루프 불변식도 인터넷에 있는 여러 이야기들을 듣다보니 명확하게 알기 힘든 부분이 있다.

그럼에도 여러군데 흩어져 있는 내용들을 내가 이해한 것과 아래의 명제를 바탕으로 조립하여 썰을 풀어보려고 한다.

루프 불변식은 루프안에서 항상 참이되는 식이다

루프 불변식 + 종료 조건 => 골

많은 이들이 추천한 maimi 학교의 루프불변식 설명은, 각 예제마다 루프불변식을 기술함으로써 루프불변식에 대한 이해를 돕는다. 그리고 붉은색으로 루프불변식 + 종료조건 => 골이라는 명제도 기술해준다.

이 글을 읽으면 루프불변식은,

• 프로그램의 목적(구하고자 하는바)과 관계가 있으며
• 루프안의 상태와 관련이 있다.

라는 결론에 도달한다.

P & !B ==> R

• P (the invariant)
• B (guard of the loop / 종료조건)
• R (postcondition) / Q (the precondition)

또다른 깔끔이 설명중의 하나가 uofs에서 설명해주는 루프불변식이다. 이 설명에 따르면, 루프가 종료되었다하더라도 R (post condition)을 만족시키기 위해서는 P가 참이어야 한다. 즉 루프불변식은,

• 루프가 종료되어도 참이어야 한다.

make-pair-예제에서의 불변식

루프안에서 변경되는 상태와 프로그램의 목적에 관련되어있다면, 분명 part1은 루프 불변식과 관련이 있다. 그래서 처음 생각해본 루프불변식은

1. a, a’

   a -> a’ after next_perm(a)

2. 원소(a) == 원소(a’)
3. a’ != a, 생성된 a’는 유일

그런데, next_perm은 false를 리턴하더라도 배열을 내림차순의 제일 작은 순서로 바꾸어 버린다. 따라서 P & !B ==> R에 따르면, 3번 항목은 프로그램을 구하는데 매우 중요한 정보이기는 하나 루프 안에서만 참인 항목이므로 루프 불변식에는 포함될수 없다.

루프 불변식의 의의(?)

모든 루프를 가진 프로그램에서 프로그램의 목적에 가장 부합하는 루프 불변식이 있는것은 아니기 때문에 루프 불변식을 찾아 리뷰를 하는게 모든 알고리즘 점검에 적합하지는 않는것 같다. 다만 루프 불변식이 프로그램의 목적에 부합하게 작성을 하고, 불변식을 점검하면 좀더 기계적인 점검이 가능할 것이다.

• 루프 안의 상태에 관심을 기울인다.
• 프로그램의 전체 탐색범위와 루프의 탐색범위 관계를 고민한다.
• (탐색 범위 안에서 항상 참이 되는 식이 있는지 생각해본다.)

make-pair 예저에서는 탐색범위가 루프 안에서 끝나버렸기 때문에 루프불변식의 중요도가 많이 희석되었지만, 루프 밖에서 프로그램의 목적을 달성하기 위해 무엇인가 추가 작업이 있다면, 루프 불변식이 많은 도움이 될것이다.