loop invariant 란 루프를 돌 동안 유지되어야 하는 statement 들이다. Loop invariant 를 체크해 봄으로써 루프가 완성적인지 아닌지 체크해 볼 수 있으므로,알고리즘을 짤 때, 특히 루프를 사용할 때 루프 점검에 아주 탁월한 방법이다. Loop invariant 에는 세 가지의 요구조건이 있다.
1. Initialization (precondition)
2. Maintanance
3. Termination (postcondition)
아래의 파일을 참조하세요.
Loop invariant.pdf
