Signals and System을 공부할 때,
System의 properties 중 Time-Invariant라는 성질이 있다.
이게 의미하는 바는 System의 Output이 시간에 관계없이 유지된다는 건데..
즉, Invariant라는 말은 불변성이라는 의미를 가지고 있다.
그렇다면 Loop Invariant란?
Loop에 관계 없이 어떠한 것이 일정하다는 의미를 가진다.
또한 이 Loop Invariant를 점검함으로, 해당 Loop가 완성적인지 아닌지를 알아 낼 수 있다.
Loop Invariant에는 다음 세 가지의 요구 조건이 있다.
1. Initialization - precondition
Loop에 들어가기 직전에, Variable의 변화 및, Statement(조건)의 변화가 맞는지 판단
for문에서 초기화문과 조건문에 해당한다고 생각하면 맞을 듯 싶다.
2. Maintenance
Loop안의 명령들에 해당하는 것으로, 이 명령들이 Loop의 목적, 즉 어떤 Algorithm의 목적에 부합하는지를 판단
각 Loop문들에서 Blocking 된 statement들이라고 보면 됨
3. Termination - postcondition
Loop종료 후 원하는 결과를 도출했느지를 판단
위 3가지를 모두 만족한다면 그 loop는 이상이 없다고 판단한다.
이 때, 최적화와는 별개의 문제
