루프 불변량

컴퓨터 과학에서, 루프 불변량은 각 반복 전후에 참인 프로그램 루프의 특성입니다.이것은 논리적인 어설션이며, 어설션 호출에 의해 코드 내에서 확인되는 경우가 있습니다.루프의 영향을 이해하려면 불변성을 아는 것이 필수적입니다.

공식 프로그램 검증, 특히 Floyd-Hoare 접근에서 루프 불변량은 형식 술어 논리에 의해 표현되며 루프의 특성 및 루프를 사용하는 확장 알고리즘에 의해 사용됩니다.루프 불변량은 루프에 들어갈 때와 반복할 때마다 참이 됩니다.따라서 루프에서 나갈 때 루프 불변량과 루프 종단 조건이 모두 보증됩니다.

프로그래밍 방법론의 관점에서 보면, 루프 불변량은 루프의 보다 추상적인 사양으로 볼 수 있으며, 이 구현의 세부사항을 넘어 루프의 더 깊은 목적을 특징짓는다.조사 기사는 컴퓨터 과학의 많은 분야(검색, 정렬, 최적화, 산술 등)의 기본 알고리즘을 다루며, 불변성의 관점에서 각각의 알고리즘을 특징짓는다.

루프와 재귀 프로그램의 유사성 때문에 불변과 함께 루프의 부분적 정확성을 증명하는 것은 유도를 통해 재귀 프로그램의 정확성을 증명하는 것과 매우 유사하다.실제로 루프 불변량은 주어진 루프와 동등한 재귀 프로그램에 대해 증명되는 귀납 가설과 같은 경우가 많다.

비공식적인 예

다음 Csubroutine max()인수 배열의 최대값을 반환합니다.a[]의 길이를 지정했다.n최소 1 입니다.코멘트는 3, 6, 9, 11 및 13 행에 기재되어 있습니다.각 코멘트는 함수의 해당 단계에서 하나 이상의 변수 값에 대해 어설션을 수행합니다.루프 본체 내에서 강조 표시된 어설션(6행과 11행)은 루프의 시작과 끝부분에서 완전히 동일합니다.따라서 이들은 루프의 불변 속성을 기술합니다.회선 13에 도달해도 이 불변성은 유지되며 루프 상태는i!=nfalse가 되었습니다.두 속성을 모두 합치면m의 최대값과 같습니다.a[0...n-1]즉, 올바른 값이 14행에서 반환되는 것입니다.

인트 맥스.(인트 n, 컨스턴트 인트 a[]) {     인트 m = a[0];     // m은 a [0...]의 최대값입니다.0]     인트 i = 1;     하는 동안에 (i != n) {         // m은 a [0...i-1]의 최대값입니다.         한다면 (m < > a[i])             m = a[i];         // m은 a [0...]의 최대값입니다.i]         ++i;         // m은 a [0...i-1]의 최대값입니다.     }     // m은 a [0...i-1]의 최대값이며 i==n     돌아가다 m; }

방어적 프로그래밍 패러다임에 따라 루프 조건i!=n5번째 줄에 있는 것을 수정해야 합니다.i<n부정한 음의 값에 대한 무한 루프를 피하기 위해n이 코드의 변경은 직관적으로 영향을 주지 않지만, 그 정확성으로 이어지는 추론은 그 이후에만 다소 복잡해진다.i>=n는 13행에서 알 수 있습니다.그것도 얻기 위해서i<=n이 조건은 루프 불변성에 포함되어야 합니다.는 것을 쉽게 알 수 있다i<=n루프의 불변성이기도 합니다.i<n회선 6의 경우 회선 5의 (표준) 루프 상태에서 얻을 수 있습니다.i<=n이후 11번째 줄에 서서i10행에서 증가했습니다.그러나, 루프 불변수가 공식적인 프로그램 검증을 위해 수동으로 제공되어야 하는 경우, 직관적으로 너무나 명백한 특성:i<=n간과되기 일쑤입니다.

플로이드-호어 논리

Floyd의 경우 -Hoare 로직,^[2]^[3] while 루프의 부분적 정확성은 다음 추론 규칙에 의해 제어됩니다.

{\displaystyle\frac{C\land I\;\mathrm {body}\;\{I\}{{I\}\;{\mathtt {while}}\(C)\mathrm {body}\;\{\lnot C\land I\}}}}

이것은 다음을 의미합니다.

코드 $\mathrm {body}$ $\mathrm {body}$ d $\mathrm {body}$ \ $displaystyle$ \ $mathrm { body$ $}$ 에 $\mathrm {body}$ 의해 $I$ 의 속성이 보존되어 있는 경우, 보다 정확하게는 $C$ 와 $I$ 가 사전에 보유되어 있을 때마다 $\mathrm {body}$ $\mathrm {body}$ d $\mathrm {body}$ $실행$ 후에 $보유$ 하는 $경우$ (위 행)
$루프$ (하행) ${\mathtt {while}}\ (C)\ \mathrm {body}$ 에 ${\mathtt {while}}\ (C)\ \mathrm {body}$ 였던 $경우$ 루프 w $h$ i e ${\mathtt {while}}\ (C)\ \mathrm {body}$ ( ${\mathtt {while}}\ (C)\ \mathrm {body}$ ) b o d ${\mathtt {while}}\ (C)\ \mathrm {body}$ (\ $displaystyle {while}\$ ( $C)$ \ $mathrm {body}$ ${\mathtt {while}}\ (C)\ \mathrm {body}$ 실행 ${\mathtt {while}}\ (C)\ \mathrm {body}$ 에는 각각 false 및 true임을 보증합니다.

즉, 다음과 같습니다.위의 규칙은 Hoare triple $\{C\land I\}\;\mathrm {body} \;\{I\}$ $\{C\land I\}\;\mathrm {body} \;\{I\}$ I $\{C\land I\}\;\mathrm {body} \;\{I\}$ $\{C\land I\}\;\mathrm {body} \;\{I\}$ $\{C\land I\}\;\mathrm {body} \;\{I\}$ $\{C\land I\}\;\mathrm {body} \;\{I\}$ y { $\{C\land I\}\;\mathrm {body} \;\{I\}$ $}$ { $displaystyle$ \ { $C$ \ $land$ I \ } \ ; \ $mathrm { body$ } \ $;\{$ 를 전제로 하는 연역적 단계입니다. $I$ 이 3배는 실제로 기계 상태에 대한 관계입니다. $C\land I$ C $C\land I$ I ( \ $displaystyle$ C \ $land$ I )가 $C\land I$ true인 상태에서 $\mathrm {body}$ $\mathrm {body}$ d $\mathrm {body}$ y ( \ $displaystyle$ \ $mathrm$ { body $\mathrm {body}$ 라는 이름의 코드를 정상적으로 실행한 경우 머신이 true $상태$ 가 될 때마다 유지됩니다.이 관계가 증명될 경우 이 ${\mathtt {while}}\ (C)\ \mathrm {body}$ 에 따라 프로그램 w ${\mathtt {while}}\ (C)\ \mathrm {body}$ i ${\mathtt {while}}\ (C)\ \mathrm {body}$ ( C ) ${\mathtt {while}}\ (C)\ \mathrm {body}$ ${\mathtt {while}}\ (C)\ \mathrm {body}$ d y ( \ $display$ style { while $}$ \ ( $C$ ) \ $mathrm$ { body $}$ 의 ${\mathtt {while}}\ (C)\ \mathrm {body}$ 실행은 I가 $\lnot C\land I$ 된 $상태$ 에서 $I$ 가 C $\lnot C\land I$ $\$ style \ $land$ 가 $\lnot C\land I$ 아닌 $\lnot C\land I$ I를 유지하는 상태로 이어집니다.이 규칙에서 $부울식$ I은 루프 불변이라고 불립니다.

예

다음 예시는 이 규칙이 어떻게 기능하는 예를 나타냅니다.프로그램을 고려하다

반면 (x < 10) x := x+1;

그러면 다음 Hoare 트리플을 증명할 수 있다.

\displaystyle \{x\leq 10\};{\mathtt {while}}\(x<10)\x:=x+1\;\{x=10\}

의 조건 Cwhile $x<10$ 은 x $x<10$ < $x<10$ $\$ $display style$ x < $10$ 。유용한 루프 불변량입니다. $x$ it $x\leq 10$ \ $display x$ \ $leq$ 10 이 적절하다는 $x\leq 10$ $x\leq 10$ 이 판명됩니다.이러한 가정 하에서 다음과 같은 3중항목을 증명할 수 있다.

{\displaystyle\{x\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}

이 트리플은 할당을 지배하는 Floyd-Hoare 로직의 규칙에서 정식으로 도출될 수 있지만 직관적으로도 정당화된다.계산은 x $x<10\land x\leq 10$ < $x<10\land x\leq 10$ x $x<10\land x\leq 10$ $x<10\land x\leq 10$ ${$ $displaystyle$ x < $10$ \ $land$ x \ $leq$ 10 $x<10\land x\leq 10$ } 이 $x<10\land x\leq 10$ 참인 $x<10\land x\leq 10$ 에서 시작됩니다.즉 $x<10$ x < $x<10$ $\$ $display style$ x < $10$ } 이 $x<10$ 참임을 $x<10$ 합니다.이 계산은 $x$ 에 1을 더합니다.즉, ${\$ 10( $정수 x의 경우)$ 이 $x\leq 10$ 여전히 참임을 의미합니다.

이 전제 하에, 규칙whileloops에서는 다음 결론을 내릴 수 있습니다.

\displaystyle \{x\leq 10\};{\mathtt {while}}\(x<10)\x:=x+1\;\lnot(x<10)\land x\leq 10\}

단, 사후 조건 $\lnot (x<10)\land x\leq 10$ ( $\lnot (x<10)\land x\leq 10$ < $\lnot (x<10)\land x\leq 10$ ) $\lnot (x<10)\land x\leq 10$ x $\lnot (x<10)\land x\leq 10$ 10 ( x < $10 )\lnot$ ( x < $10$ )\ $land x\leq$ 10 $\lnot (x<10)\land x\leq 10$ ) $\lnot (x<10)\land x\leq 10$ ( $x$ 는 10 이하다, 그러나 10 이하다)는 $x=10$ 으로 x $x=10$ = 10 (x $style$ x $= 10$ 과 $x=10$ .

$0\leq x$ 0 $0\leq x$ $($ \ $displaystyle$ 0 \ $leq$ x )는 $0\leq x$ 이 루프 예의 다른 불변이며, 사소한 속성 $\mathrm {true}$ $\mathrm {true}$ e $\mathrm {true}$ \ $displaystyle$ \ $mathrm$ { $true }$ 는 $\mathrm {true}$ $\mathrm {true}$ 것입니다.전 고정 수익률 이상의 추론 규칙을 적용하면 whil e()<>10)x:=x+1{10≤)}{\displaystyle\와 같이{0\leq)}\,{\mathtt{는 동안}})(x< 10분)\ x:=x+1\, \{10\leq x\}}. 고정 tr우라늄 e{\displaystyle \mathrm{사실}에}{tr우라늄 e}whil e()<>10)이 열린다를 적용하는 것은{0≤)}.x:\ $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ + $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ { $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ x $}$ { $displaystyle$ \ { \ $mathrm$ { $true }$ \ ; { \ $mathtt$ { $while }$ \ ( x < $10$ ) \ x : $= x$ + $1$ \ ; \ { $10$ \ $leq$ x \ $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ } $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ 。이것은 조금 더 표현력이 있습니다.

프로그래밍 언어 지원

에펠

에펠 프로그래밍 언어는 루프 ^[4]불변량을 기본적으로 지원합니다.루프 불변량은 클래스 불변량과 동일한 구문으로 표현된다.다음 예제에서 루프 불변식은x <= 10루프 초기화 후 및 루프 본체의 각 실행 후에 true여야 합니다.이것은 실행 시 체크됩니다.

    부터         x := 0     불변의         x <=> 10     까지         x > 10     고리         x := x + 1     끝.

와일

Whyy 프로그래밍 언어도 루프 불변량을 ^[5]1등급으로 지원합니다.루프 불변량은 하나 이상의 값을 사용하여 표현됩니다.where다음 예시와 같이 절을 지정합니다.

기능. 맥스.(인트[] 항목들) -> (인트 r) // 최대값을 계산하려면 하나 이상의 요소가 필요합니다. 필요.  항목들  > 0 // (1) 어떤 요소보다 작지 않은 결과 보증하다 모든. { i 에 0.. 항목들    항목들[i] <=> r } // (2) 결과가 하나 이상의 요소와 일치합니다. 보증하다 몇개 { i 에 0.. 항목들    항목들[i] == r }:     //     내트 i = 1     인트 m = 항목들[0]     //     하는 동안에 i < >  항목들      // (1) 지금까지 m보다 큰 항목은 없습니다.     어디에 모든. { k 에 0..i   항목들[k] <=> m }     // (2) 지금까지 본 1개 이상의 항목이 m과 일치합니다.     어디에 몇개 { k 에 0..i   항목들[k] == m }:         한다면 항목들[i] > m:             m = 항목들[i]         i = i + 1     //     돌아가다 m

그max()함수는 정수 배열에서 가장 큰 요소를 결정합니다.이를 정의하려면 배열에 하나 이상의 요소가 포함되어 있어야 합니다.의 전제 조건max()반환되는 값은 (1) 어떤 요소보다 작지 않아야 하며 (2) 적어도 하나의 요소와 일치해야 한다.루프 불변량은 유도적으로 정의됩니다.where각 절은 사후 조건의 절에 대응합니다.근본적인 차이점은 루프 불변성의 각 절이 결과가 현재 요소까지 올바른 것으로 식별한다는 것입니다.i그러나 사후 조건은 결과가 모든 요소에 대해 올바른 것으로 식별됩니다.

루프 불변량 사용

루프 불변수는 다음 중 하나의 목적으로 사용할 수 있습니다.

순전히 다큐멘터리
어설션 콜에 의해 코드 내에서 체크되다
Floyd-Hoare 접근법에 따라 검증된다.

1. 자연어 댓글 (예:// m equals the maximum value in a[0...i-1](상기의 예에서는)로 충분합니다.

2.의 경우 C 라이브러리 assert.h 또는 위의 그림과 같은 프로그래밍 언어 지원이 필요합니다.invariant에펠의 조항.대부분의 경우 런타임 체크는 컴파일러 또는 런타임 ^{[citation needed]}옵션에 의해 실행 디버깅을 위해 켜거나 끌 수 있습니다.

3.의 경우, 수학적인 증명을 지원하기 위한 몇 가지 툴이 존재합니다.보통 위의 Floyd를 기반으로 합니다.Hoare 규칙. 실제로 특정 루프 코드가 특정 루프 불변성을 충족합니다.

추상 해석 기술을 사용하여 주어진 코드의 루프 불변성을 자동으로 검출할 수 있습니다.단, 이 접근방식은 매우 단순한 불변량(예:0<=i && i<=n && i%2==0).

루프 불변 코드와의 구별

루프 불변 코드는 프로그램 의미론에 영향을 주지 않고 루프 본문 밖으로 이동할 수 있는 문 또는 식으로 구성됩니다.루프 불변 코드 모션이라고 불리는 이러한 변환은 프로그램을 최적화하기 위해 일부 컴파일러에 의해 수행됩니다.루프 불변 코드의 예(C 프로그래밍 언어)는 다음과 같습니다.

위해서 (인트 i=0; i< >n; ++i) {     x = y+z;     a[i] = 6*i + x*x; }

계산하면x = y+z그리고.x*x루프 전에 이동할 수 있으므로 동등하지만 더 빠른 프로그램이 생성됩니다.

x = y+z; t1 = x*x; 위해서 (인트 i=0; i< >n; ++i) {     a[i] = 6*i + t1; }

이와는 대조적으로, 예를 들어, 자산0<=i && i<=n는 원래 프로그램과 최적화된 프로그램 모두에 대해 루프 불변이지만 코드의 일부가 아니기 때문에 "루프 밖으로 이동"이라고 하는 것은 의미가 없습니다.

루프 불변 코드는 대응하는 루프 불변 ^{[clarification needed]}속성을 유도할 수 있습니다.위의 예에서 가장 쉽게 확인할 수 있는 방법은 루프 전 및 루프 내에서 모두 루프 불변 코드가 계산되는 프로그램을 고려하는 것입니다.

x1 = y+z; t1 = x1*x1; 위해서 (인트 i=0; i< >n; ++i) {     x2 = y+z;     a[i] = 6*i + t1; }

이 코드의 루프 불변 속성은 다음과 같습니다.(x1==x2 && t1==x2*x2) i==0루프 전에 계산된 값이 (첫 번째 반복 ^{[citation needed]}전 제외) 내에서 계산된 값과 일치함을 나타냅니다.

「」를 참조해 주세요.

레퍼런스

^ 카를로 A푸리아, 베르트랑 메이어, 세르게이 벨더."루프 불변량: 분석, 분류 및 예시"ACM Computing Surveies, vol. 46, 제3호, 2014년 2월 ([1])
^ Robert W. Floyd (1967). "Assigning Meanings to Programs" (PDF). In J.T. Schwartz (ed.). Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science. Vol. 19. Providence, RI: American Mathematical Society. pp. 19–32.
^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. Archived from the original (PDF) on 2016-03-04.
^ 마이어, 베르트랑, 에펠: 언어, 프렌티스 홀, 1991, 페이지 129-131.
^ Pearce, David J.; Groves, Lindsay (2015). "Designing a Verifying Compiler: Lessons Learned from Developing Whiley". Science of Computer Programming. 113: 191–220. doi:10.1016/j.scico.2015.09.006.

추가 정보

토마스 H. 코먼, 찰스 E. 리저슨, 로널드 L. 리베스트, 클리포드 스타인.알고리즘 소개, 제2판MIT Press and McGraw-Hill, 2001.ISBN 0-262-03293-7.17~19페이지, 섹션 2.1: 삽입 정렬.
데이비드 그리즈."루프 불변성과 루프를 개발하기 위한 표준 전략에 대한 메모"컴퓨터 프로그래밍의 과학, 제2권, 207~214쪽. 1984.
마이클 D.에른스트, 제이크 코크렐, 윌리엄 그리즈월드, 데이비드 노킨"프로그램의 진화를 지원할 가능성이 높은 프로그램의 불변성을 동적으로 검출합니다."소프트웨어 엔지니어링에 관한 국제회의, 1999년 페이지 213-224.
로버트 페이지.「불변량을 사용한 프로그래밍」IEEE 소프트웨어, 3 (1):56~69.1986년 1월
옌홍아류, 스콧 D.스톨러와 팀 테이텔바움.효율적인 계산을 위한 불변량 강화.컴퓨터 프로그래밍 과학, 41(2): 139~172.2001년 10월
마이클 허스, 마크 라이언"컴퓨터 공학 논리", 제2판

[1] 카를로 A푸리아, 베르트랑 메이어, 세르게이 벨더."루프 불변량: 분석, 분류 및 예시"ACM Computing Surveies, vol. 46, 제3호, 2014년 2월 ([1])

[2] Robert W. Floyd (1967). "Assigning Meanings to Programs" (PDF). In J.T. Schwartz (ed.). Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science. Vol. 19. Providence, RI: American Mathematical Society. pp. 19–32.

[3] Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. Archived from the original (PDF) on 2016-03-04.

[4] 마이어, 베르트랑, 에펠: 언어, 프렌티스 홀, 1991, 페이지 129-131.

[5] Pearce, David J.; Groves, Lindsay (2015). "Designing a Verifying Compiler: Lessons Learned from Developing Whiley". Science of Computer Programming. 113: 191–220. doi:10.1016/j.scico.2015.09.006.

[2]

[3]

[4]

[5]

Search

루프 불변량

네임스페이스

더

목차

비공식적인 예

플로이드-호어 논리

예

프로그래밍 언어 지원

에펠

와일

루프 불변량 사용

루프 불변 코드와의 구별

「」를 참조해 주세요.

레퍼런스

추가 정보

Search

루프 불변량

비공식적인 예

플로이드-호어 논리

예

프로그래밍 언어 지원

에펠

와일

루프 불변량 사용

루프 불변 코드와의 구별

「 」를 참조해 주세요.

레퍼런스

추가 정보

「」를 참조해 주세요.