루프 불변량
프로그램의 루프가 실행되는 동안 항상 참으로 유지되는 수학적 성질이다. 반복적인 연산이 포함된 알고리즘의 정확성을 정형 검증할 때 루프의 시작과 끝에서 상태가 올바름을 증명하는 핵심 도구이다.