루프 불변성
루프 불변성, 루프 불변량, 루프 불변자(Loop invariant)는 컴퓨터 과학에서 각 반복 이전(및 이후)에 적용되는 프로그램 루프의 속성이다. 이는 때때로 코드 표명(assertion)으로 확인되는 논리적 표명이다. 루프의 효과를 이해하려면 불변성을 아는 것이 필수적이다.
공식적인 프로그램 검증, 특히 플로이드-호어 접근법에서 루프 불변량은 형식적 술어 논리로 표현되고 루프의 속성을 증명하는 데 사용되며 루프(일반적으로 정확성 속성)를 사용하는 확장 알고리즘에 의해 사용된다. 루프 불변성은 루프에 들어갈 때와 각 반복 후에 참이 되므로 루프에서 나갈 때 루프 불변성과 루프 종료 조건이 모두 보장될 수 있다.
프로그래밍 방법론 관점에서 루프 불변은 루프의 보다 추상적인 사양으로 볼 수 있으며, 이는 이 구현의 세부 사항을 넘어 루프의 더 깊은 목적을 특징으로 한다. 설문 조사 기사는 컴퓨터 과학의 다양한 영역(검색, 정렬, 최적화, 산술 등)의 기본 알고리즘을 다루며 불변의 관점에서 각 알고리즘을 특성화한다.
루프와 재귀 프로그램의 유사성 때문에 불변성을 사용하여 루프의 부분 정확성을 증명하는 것은 귀납법을 통해 재귀 프로그램의 정확성을 증명하는 것과 매우 유사하다. 실제로 루프 불변은 주어진 루프와 동등한 재귀 프로그램에 대해 증명되는 귀납적 가설과 동일한 경우가 많다.
비공식 예제
[편집]int max(int n, const int a[]) {
int m = a[0];
// m equals the maximum value in a[0...0]
int i = 1;
while (i != n) {
// m equals the maximum value in a[0...i-1]
if (m < a[i])
m = a[i];
// m equals the maximum value in a[0...i]
++i;
// m equals the maximum value in a[0...i-1]
}
// m equals the maximum value in a[0...i-1], and i==n
return m;
}