호어 논리 문서 원본 보기

{{위키데이터 속성 추적}}
'''호어 논리'''({{Llang|en|Hoare logic}}), '''플로이드-호어 논리'''({{Llang|en|Floyd-Hoare logic}}) 또는 '''호어 규칙'''({{Llang|en|Hoare rules}})은 {{임시 링크|정확성 (컴퓨터 과학)|en|Correctness (Computer Science)|label=컴퓨터 프로그램의 정확성(correctness)}} 엄격하게 추론하기 위한 일련의 논리적 규칙을 갖춘 [[형식 체계]]이다. 1969년 영국의 컴퓨터 과학자이자 [[수리 논리학|논리학자]]인 [[토니 호어]]는 호어 논리를 제안하였고, 이후 호어와 다른 연구자들이 호어 논리를 개선하였다.<ref name="hoare">{{저널 인용|제목=An axiomatic basis for computer programming|저널=[[Communications of the ACM]]|성=Hoare|이름=C. A. R.|저자링크=토니 호어|url=https://dl.acm.org/doi/pdf/10.1145/363235.363259|날짜=October 1969|권=12|호=10|쪽=576&ndash;580|doi=10.1145/363235.363259}}</ref> 원래 아이디어는 [[순서도]]에 대해 유사한 체계를 발표한 [[로버트 플로이드]]의 작업에서 비롯되었다.<ref>{{저널 인용|제목=Assigning meanings to program|저널=Proceedings of the American Mathematical Society Symposia on Applied Mathematics|성=Floyd|이름=R. W.|url=https://www.cs.tau.ac.il/~nachumd/term/FloydMeaning.pdf|저자링크=로버트 플로이드|권=19|쪽=19&ndash;31|날짜=1967}}</ref>

== 호어 세 쌍 ==
호어 논리의 핵심 특징은 '''호어 세 쌍'''({{Llang|en|Hoare triple}})이다. 호어 세 쌍은 명령을 실행하는 것이 계산 상태를 어떻게 바꾸는지 설명한다. <math>P</math>와 <math>Q</math>가 '''[[표명]]'''({{lang|en|assertion}})이고 <math>C</math>가 '''명령'''({{lang|en|command}})일 때,  호어 세 쌍은 <math>\{P\} C \{Q\}</math>와 같은 형태이다.<ref group="note">호어의 원래 논문에서는 "<math>\{P\}C\{Q\}</math>" 대신 "<math>P\{C\}Q</math>"이 사용되었다.</ref>
이때 <math>P</math>는 '''전제 조건'''({{lang|en|precondition}}), <math>Q</math>는 '''사후 조건'''({{lang|en|postcondition}})으로, 위의 호어 세 쌍은 전제 조건이 충족된 상태에서 명령을 실행하였을 때 사후 조건이 성립함을 나타낸다. 각 표명은 [[1차 논리]]의 논리식이다.

호어 논리는 간단한 [[명령형 프로그래밍|명령형 프로그래밍 언어]]의 모든 구성에 대한 [[공리]]와 [[추론 규칙]]을 제공한다. 호어의 원본 논문에 있는 간단한 언어에 대한 추론 규칙 외에도, 호어를 비롯한 많은 연구자들은 다른 언어 구성에 대한 추론 규칙을 개발하였다. 예시로는 [[병행성|동시성]], [[함수 (컴퓨터 과학)|프로시저]], [[브랜치 (컴퓨터 과학)|점프]] 및 [[포인터 (프로그래밍)|포인터]]에 대한 추론 규칙이 있다.

== 부분 정확성과 총 정확성 ==
호어 세 쌍은 직관적으로 다음과 같은 뜻을 갖는다: 모든 상태에 대해, 상태가 <math>C</math>를 실행하기 전에 <math>P</math>를 만족하고, <math>C</math>를 실행하여 종료되었을 때, 그 결과 상태는 <math>Q</math>를 만족한다. 만약 <math>C</math>가 종료되지 않는다면 <math>Q</math>가 임의의 표명이더라도 호어 세 쌍은 유효하다. 이는 '종료된 이후의 상태'가 존재하지 않기 때문에, "종료된 이후의 상태는 <math>Q</math>를 만족한다"라는 명제가 공허하게 참이 된다고 설명할 수 있다. 예를 들어, <math>Q</math>를 false로 선택하면 <math>C</math>는 항상 종료되지 않는다는 것을 표현할 수 있다.

즉, 호어 논리는 프로그램의 '''부분 정확성'''({{lang|en|partial correctness}})만을 검증한다. '''총 정확성'''({{lang|en|total correctness}})을 보이기 위해서는 명령이 '''종료'''({{lang|en|termination}})하는지 추가로 검증해야 한다. 이는 별도의 방법을 사용하거나 반복문 규칙을 확장하여 증명할 수 있다.<ref name="Reynolds.2009">{{서적 인용|제목=Theories of Programming Languages|성=John C. Reynolds|저자링크=John C. Reynolds|연도=2009|출판사=Cambridge University Press}}) Here: Sect. 3.4, p. 64.</ref>

이 문서에서 '종료'는 계산이 언젠가 완료된다는 더 넓은 의미로 사용되고, 계산에 무한 루프가 없음을 의미한다. 이는 0으로 나누기 등 프로그램을 곧바로 중지시키는 구현 제한 위반이 없다는 것을 의미하지 않는다. 1969년 논문에서 호어는 구현 제한 위반이 없음을 수반하는 더 좁은 종료 개념을 사용하였다. 호어는 더 넓은 종료 개념을 선호한다고 하였는데, 그러한 개념이 표명의 구현 독립성을 유지하기 때문이다.<ref>Hoare (1969), p.578-579</ref>

== 추론 규칙 ==

=== 빈 명령 공리 도식 ===
'''[[NOP (코드)|빈 명령]] 공리 도식'''({{lang|en|empty statement axiom schema}})은 다음과 같다.<ref group="note">호어 규칙을 [[자연 연역]] 표현법으로 표현하였다. 예를 들어, <math>\dfrac{\alpha,\beta}{\phi}</math>는 "{{수학 변수|&alpha;}}와 {{수학 변수|&beta;}}가 성립한다면 {{수학 변수|&phi;}}가 성립한다"를 의미한다. {{수학 변수|&alpha;}}, {{수학 변수|&beta;}}는 추론 규칙의 '''전제'''({{lang|en|premise}})이고, {{수학 변수|&phi;}}는 추론 규칙의 '''결론'''({{lang|en|conclusion}})이다. 전제가 없는 추론 규칙을 '''공리'''({{lang|en|axiom}})라고 하고, <math>\dfrac{}{\quad\phi\quad}</math>으로 표기한다.</ref>

: <math>\dfrac{}{\{P\}\texttt{skip}\{P\}}</math>

{{모노|skip}} 문은 프로그램의 상태를 변경하지 않으므로, 실행 이전에 참이었던 것은 무엇이든 실행 이후에도 마찬가지로 참임을 나타낸다.

=== 할당 공리 도식 ===
'''할당 공리 도식'''({{lang|en|assignment axiom schema}})은 다음과 같다.

: <math>\dfrac{}{\{P[E/x]\} x := E \{P\}}</math>

변수 {{수학 변수|x}}를 [[자유 변수와 종속 변수|자유 변수]]로 갖는 표명 {{수학 변수|P}}에 대해, <math>P[E/x]</math>는 {{수학 변수|P}}에서 [[자유 변수와 종속 변수|자유롭게 나타나는]] {{수학 변수|x}}를 각각 표현 {{수학 변수|E}}로 [[치환 실례|치환]]하여 얻은 표명을 나타낸다.

할당 공리 도식은 <math>P[E/x]</math>의 진리값은 할당 이후의 {{수학 변수|P}}의 진리값과 같다는 것을 의미한다. 따라서 <math>P[E/x]</math>이 할당 이전에 참이라면 할당 이후 {{수학 변수|P}}는 참이다. 한편 공리 도식에서 표명 <math>\neg P</math>를 사용하면, <math>\neg P[E/x]</math>이 할당 이전에 참일 때 할당 이후 <math>\neg P</math>가 참이라는 명제를 얻는다. 따라서 할당 공리의 이 또한 성립하는데, 할당 이전에 <math>P[E/x]</math>이 거짓이라면 할당 이후 {{수학 변수|P}}는 거짓이다.

유효한 세 쌍의 예는 다음과 같다.

:* <math>\{ x+1 = 43 \}  y := x + 1  \{ y = 43 \}</math>
:* <math>\{ x + 1 \leq N \} x := x + 1 \{ x \leq N \}</math>

치환을 통해 바뀌지 않은 전제조건은 모두 사후조건으로 넘어갈 수 있다. 첫 번째 예에서는 할당 <math>y:=x+1</math>이후에도 <math>x+1=43</math>이라는 사실은 변하지 않으므로 표명 <math>x+1=43</math>은 사후 조건에 나타날 수 있다. 엄밀하게는, {{수학 변수|P}}를 "<math>y=43</math> 그리고 <math>x+1=43</math>"으로 놓고 공리 도식을 적용하여 얻을 수 있다. 이때 전제 조건 <math>P[(x+1)/y]</math>는 "<math>x+1=43</math> 그리고 <math>x+1=43</math>"이 되는데, 이는 주어진 전제 조건인 <math>x+1=43</math>으로 단순화할 수 있다.

할당 공리 도식을 통해 전제 조건을 찾기 위해서는 우선 사후 조건을 선택한 후 할당의 좌변에 있는 모든 변수를 할당의 우변에 있는 표현으로 치환하여야 한다. 이 과정에서 전제 조건과 사후 조건을 바꾼 <math>\{P\} x:=E \{P[E/x]\}</math>는 올바르지 않은 규칙이므로 주의하여야 한다. <math>\{ x = 5 \} x := 3 \{ 3 = 5 \}</math>가 이 규칙의 반례가 된다.
언뜻 보기에 올바를 것 같은 <math>\{P\} x:=E \{P \wedge x=E\}</math> 또한 올바르지 않은 규칙이다. <math>\{ x = 5 \}  x := x + 1  \{ x = 5 \wedge x = x + 1 \}</math>가 이 규칙의 반례가 된다.

주어진 사후 조건 {{수학 변수|P}}이 전제 조건 <math>P[E/x]</math>을 유일하게 결정하는 반면, 역은 성립하지 않는다. 다음 호어 세 쌍들은 모두 할당 공리 도식의 유효한 예시이고 같은 전제 조건을 가지고 있지만 서로 다른 사후 조건을 갖는다.

:* <math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}  x := y \cdot y  \{ 0 \leq x \wedge x \leq 9 \}</math> ,
:* <math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}  x := y \cdot y  \{ 0 \leq x \wedge y\cdot y \leq 9 \}</math>,
:* <math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}  x := y \cdot y  \{ 0 \leq y\cdot y \wedge x \leq 9 \} </math>,
:* <math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}  x := y \cdot y  \{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}</math>


호어가 제안한 할당 공리는 둘 이상의 이름이 동일한 저장된 값을 참조할 수 있는 경우 적용되지 않는다. 예를 들어, 호어 세 쌍 <math>\{ y = 3 \}  x := 2  \{ y = 3 \}</math>은 <math>\{P\}</math>와 <math>\{P[2/x]\}</math>를 <math>\{y=3\}</math>으로 놓아서 얻을 수 있으므로 할당 공리 도식의 유효한 예시이다. 하지만, {{수학 변수|x}}와 {{수학 변수|y}}가 동일한 변수를 참조하는 경우(앨리어싱) 이는 올바르지 않다.

=== 합성 규칙 ===
{| class="wikitable collapsible collapsed" align="right"
!보조 변수 없는 swap 명령 검증
|-
|
{| style="border:1px solid grey;"
|+ 아래의 세 명령(2, 4, 6행)은 변수 {{수학 변수|a}}와 {{수학 변수|b}}의 값을 보조 변수 없이 교환한다. 증명에서 {{수학 변수|a}}와 {{수학 변수|b}}의 초기값은 각각 상수 {{수학 변수|A}}와 {{수학 변수|B}}로 표시하였다. 증명은 7행부터 거꾸로 읽는 것이 가장 좋다. 예를 들어, 5행은 7행에서 {{수학 변수|a}} (6행의 대상 표현식)를 <math>a-b</math> (6행의 소스 표현식)으로 대체하여 얻는다.  . <math>a-(a-b) = b</math> (5행→3행), <math>a+b-b = a</math> (3행→1행)와 같은 산술 표현 단순화가 암묵적으로 사용되었다.
| '''번호'''
| '''명령'''
| colspan="6" | '''표명'''
|-
| '''1:'''&nbsp;&nbsp;&nbsp;
|
|<math>\{a = A \wedge b = B \}</math>
|-
| '''2:'''
| <math>a := a + b;</math>&nbsp;&nbsp;&nbsp;
|-
|'''3:'''
|
| <math>\{ a - b = A \wedge b = B \}</math>
|-
| '''4:'''
| <math>b := a - b;</math>
|-
| '''5:'''
|
| <math>\{b=A\wedge a-b=B\}</math>
|-
| '''6:'''
| <math>a := a - b</math>
|-
| '''7:'''
|
| <math>\{b= A\wedge a = B \}</math>
|}
|}
'''합성 규칙'''({{lang|en|rule of composition}})은 다음과 같다.<ref>{{서적 인용|url=http://www.cs.bham.ac.uk/research/projects/lics/|제목=Logic in Computer Science|성=Huth|이름=Michael|성2=Ryan|이름2=Mark|날짜=2004-08-26|판=second|출판사=CUP|쪽=276|isbn=978-0521543101}}</ref>

: <math>\dfrac{\{P\} S \{Q\}\quad,\quad  \{Q\} T \{R\}}{\{P\} S;T \{R\}}</math>

프로그램 {{수학 변수|S}}가 실행된 이후 프로그램 {{수학 변수|T}}를 실행하는 (즉 {{수학 변수|S}}, {{수학 변수|T}}를 순차적으로 실행하는) 프로그램을 <math>S;T</math>으로 표기한다. 이때 {{수학 변수|Q}}는 '''중간 조건'''({{lang|en|midcondition}})이라고 부른다.

예를 들어, 할당 공리의 다음 두 가지 예시
: <math>\{ x + 1 = 43 \}  y := x + 1  \{ y = 43 \}</math>, <math>\{ y = 43 \}  z := y  \{ z = 43 \}</math>
에서, 합성 규칙을 적용하여
: <math>\{ x + 1 = 43 \}  y := x + 1; z := y  \{ z = 43 \}</math>
와 같은 결론을 얻을 수 있다.

=== 조건문 규칙 ===

: <math>\dfrac{\{B \wedge P\} S \{Q\}\quad,\quad \{\neg B \wedge P \} T \{Q\}}{\{P\} \texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif} \{Q\}}</math>

'''조건문 규칙'''({{lang|en|conditional rule}})에서, {{모노|then}}과 {{모노|else}} 부분에 공통되는 사후 조건 {{수학 변수|Q}}가 전체 조건문 {{모노|if...endif}}의 사후 조건이 된다.<ref>{{저널 인용|제목=Fifty years of Hoare's logic|저널=Formal Aspects of Computing|성=Apt|이름=Krzysztof R.|성2=Olderog|이름2=Ernst-Rüdiger|url=https://ir.cwi.nl/pub/29146|날짜=December 2019|권=31|호=6|쪽=759|doi=10.1007/s00165-019-00501-3}}</ref> {{모노|then}}과 {{모노|else}}에서는 전제 조건에 각각 {{수학 변수|B}}와  <math>\neg B</math>를 추가할 수 있다. 조건 {{수학 변수|B}}에는 부작용이 없어야 한다.

조건문 규칙은 호어의 원본 논문에는 포함되어 있지 않다.<ref name="hoare" /> 그러나

: <math>\texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif}</math>

는 일회성 반복문인

: <math>\texttt{bool}\ b:=\texttt{true};  \texttt{while}\ B\wedge b\ \texttt{do}\ S; b:=\texttt{false}\ \texttt{done};  b:=\texttt{true};  \texttt{while}\ \neg B\wedge b\ \texttt{do}\ T; b:=\texttt{false}\ \texttt{done}</math>

와 동일한 효과가 있으므로, 조건문 규칙은 다른 추론 규칙으로부터 유도할 수 있다.

비슷한 방식으로, {{모노|for}} 반복, {{모노|do...until}} 반복, {{모노|switch}}, {{모노|break}}, {{모노|continue}} 같은 다른 파생 프로그램 구성에 대한 규칙도 호어의 원본 논문의 규칙으로부터 [[프로그램 변환|프로그램을 변환하여]] 유도할 수 있다.

=== 결과 규칙 ===

: <math>\dfrac{P_1 \rightarrow P_2\quad  ,\quad  \{P_2\} S \{Q_2\}\quad  ,\quad  Q_2 \rightarrow Q_1}{\{P_1\} S \{Q_1\}}</math>

'''결과 규칙'''({{lang|en|consequence rule}})은 전제 조건을 강화하거나 사후 조건을 약화한다. 결과 규칙을 통해 얻는 새로운 호어 세 쌍은 일반적으로 전제가 되는 호어 세 쌍보다 약하지만, 원하는 것보다 더 강한 호어 세 쌍을 이미 증명하였을 때 구문론적으로 일치하는 호어 세 쌍을 얻기 위해 결과 규칙을 사용할 수 있다.

예를 들어, 다음을 검증하자.

: <math>\{0 \leq x \leq 15 \}\texttt{if}\ x<15\ \texttt{then}\ x:=x+1\ \texttt{else}\ x:=0\ \texttt{endif} \{0 \leq x \leq 15 \}</math>

조건부 규칙을 적용하여, 다음을 증명하면 충분하다.

* {{모노|then}}에 해당하는 <math>\{0 \leq x \leq 15 \wedge x < 15 \}  x:=x+1  \{ 0 \leq x \leq 15 \}</math>, 또는 단순화하여 <math>\{0 \leq x < 15 \}  x:=x+1  \{0 \leq x \leq 15 \}</math>를 증명하여야 한다.
* {{모노|else}}에 해당하는 <math>\{0 \leq x \leq 15 \wedge x \geq 15\}  x:=0  \{0 \leq x \leq 15\}</math>, 또는 단순화하여 <math>\{x=15\}  x:=0  \{0 \leq x \leq 15 \}</math>를 증명하여야 한다.

그러나, <math>P</math>를 <math>0 \le x \le 15</math>로 두어 할당 공리 도식을 적용하면 <math>\{0 \leq x+1 \leq 15\}  x:=x+1  \{0 \leq x \leq 15\}</math>, 또는 단순화하여 <math>\{-1 \leq x < 15\}  x:=x+1  \{0 \leq x \leq 15\}</math>를 얻는다. 이 호어 세 쌍의 전제는 <math>\{0 \leq x < 15\}</math>보다 약하므로, 결과 규칙을 적용하여 <math>\{0 \leq x < 15\}  x:=x+1  \{0 \leq x \leq 15\}</math>을 이끌어 내야 한다.

마찬가지로, 할당 공리 도식을 적용하면 <math>\{0 \leq 0 \leq 15\}  x:=0  \{0 \leq x \leq 15\}</math>, 또는 단순화하여 <math>\{\texttt{true}\}  x:=0  \{0 \leq x \leq 15\}</math>를 얻는다. 이 호어 세 쌍의 전제는 <math>\{x = 15\}</math>보다 약하므로, 결과 규칙을 적용하여 <math>\{x=15\}  x:=0  \{0 \leq x \leq 15 \}</math>를 이끌어 낼 수 있다.

거칠게 말해서, 결과 규칙은 너무 강한 전제로부터 얻는 정보 <math>\{x=15\}</math>를 "잊어버리는" 효과를 준다. <math>\{x=15\}  x:=0  \{0 \leq x \leq 15 \}</math>를 증명하기 위해서는 그만큼 강한 정보가 필요하지 않기 때문이다.

=== 반복문 규칙 ===
'''반복문 규칙'''({{lang|en|while rule}})은 다음과 같다.

: <math>\dfrac{\{P \wedge B\} S \{P\}}{\{P\} \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} \{\neg B \wedge P\}}</math>

여기서 {{수학 변수|P}}는 [[반복 불변량]]({{lang|en|loop invariant}})으로, 반복문의 내용 {{수학 변수|S}}에 의해 보존된다. 반복이 완료된 후 {{수학 변수|P}}는 여전히 유지되고, 반복이 종료되려면 <math>\neg B</math>가 성립하여야 한다. 조건문 규칙과 마찬가지로 {{수학 변수|B}}에는 부작용이 없어야 한다.

예를 들어,

: <math>\{x \leq 10\} \texttt{while}\ x<10\ \texttt{do}\ x:=x+1\ \texttt{done} \{\neg x < 10 \wedge x \leq 10\}</math>

는 반복문 규칙에 의해,

: <math>\{x \leq 10 \wedge x < 10\}  x := x + 1  \{x \leq 10 \}</math>, 또는 단순화하여 <math>\{x < 10\}  x := x + 1  \{x \leq 10 \}</math>
으로부터 추론할 수 있다. 이는 할당 공리 도식을 통해 쉽게 얻을 수 있다.
마지막으로 사후조건 <math>\{\neg x <10 \wedge x\leq 10\}</math>을 <math>\{x=10\}</math>으로 단순화할 수 있고, 이를 통해

: <math>\{x \leq 10\} \texttt{while}\ x<10\ \texttt{do}\ x:=x+1\ \texttt{done} \{x = 10\}</math>

와 같이 간단한 반복문 프로그램을 검증할 수 있다.

또 다른 예시로, 반복문 규칙을 사용하면 임의의 수 {{수학 변수|a}}의 정확한 제곱근 {{수학 변수|x}}를 계산하는 ― {{수학 변수|x}}가 정수 변수이고 {{수학 변수|a}} 제곱수가 아닌 경우에도 ― 다음과 같은 이상한 프로그램을 형식적으로 검증할 수 있다.

: <math>\{\texttt{true}\}  \texttt{while}\ x\cdot x \neq a\ \texttt{do}\ \texttt{skip}\ \texttt{done}  \{x \cdot x = a \wedge \texttt{true}\}</math>

{{수학 변수|P}}를 {{모노|true}}로 놓아 반복문 규칙을 적용하여, 다음을 증명하면 된다.

: <math>\{\texttt{true} \wedge x\cdot x \neq a\}  \texttt{skip}  \{\texttt{true}\}</math>

이는 결과 규칙과 빈 명령 규칙을 통해 증명할 수 있으므로, 추론 규칙을 따라 유효한 증명을 만든 것이다.
한편 이 프로그램의 반복문은 비어있고, 계속 반복한다고 하여도 계산에 진전이 없으므로 이 프로그램에 유효한 검증이 있다는 것은 이상하게 보일 수 있다. 사실, 이는 이상한 프로그램이 부분적으로 정확하다({{lang|en|partially correct}})는 것을 검증한 것이다. 만약 프로그램이 종료된다면 {{수학 변수|x}}는 (우연히) {{수학 변수|a}}의 제곱근 값을 포함하고 있음이 확실하지만, 다른 모든 경우에는 프로그램이 종료되지 않는다. 이 증명은 프로그램의 총 정확성({{lang|en|totally correct}})을 증명한 것이 아니다.

=== 총 정확성과 반복문 규칙 ===
위의 일반적인 반복문 규칙을 다음 규칙으로 대체하면 호어 대수를 사용하여 총 정확성을, 즉 부분 정확성과 종료를 함께 증명할 수도 있다. 일반적으로, 중괄호 대신 대괄호를 사용하여 프로그램 정확성에 대한 다른 개념임을 나타낸다.

: <math>\dfrac{<\ \text{is a well-founded ordering on the set}\ D\quad,\quad [P \wedge B \wedge t \in D \wedge t = z]  S  [P \wedge t \in D \wedge t < z ]}{[P \wedge t \in D]  \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done}  [\neg B \wedge P \wedge t \in D]}</math>

이 규칙에서는 반복 불변량 {{수학 변수|P}}을 유지하는 동시에, 어떤 집합 {{수학 변수|D}} 위의 [[정초 관계]] {{수학 변수|<}}에 대해 값이 절대적으로 감소하는 표현식 {{수학 변수|t}}을 사용하여 종료를 증명한다. 이러한 표현 {{수학 변수|t}}를 '''반복 변량'''({{lang|en|loop variant}})이라고 부른다. {{수학 변수|<}}는 정초 관계이므로, 절대 감소하는 {{수학 변수|D}}안의 [[전순서 집합|사슬]]은 유한한 길이만 가질 수 있다. (예를 들어, [[자연수]] <math>\mathbb{N}</math> 위의 순서 {{수학 변수|<}}는 정초 관계이다. 한편, 정수 <math>\mathbb{Z}</math>와 [[양수 (수학)|양의 실수]] <math>\mathbb{R}^+</math> 위의 순서 {{수학 변수|<}}에 대해서는 무한히 감소하는 수열을 선택할 수 있고, 이들은 정초 관계가 아니다.) 따라서 {{수학 변수|t}}는 무한히 감소할 수 없고, 유한한 길이의 실행 이후 반복문이 종료한다는 증거가 된다.

반복 불변량 {{수학 변수|P}}가 주어졌을 때, 조건 {{수학 변수|B}}는 {{수학 변수|t}}가 {{수학 변수|D}}의 [[극대 원소와 극소 원소|극소 원소]]가 아니라는 것을 이끌어내야 한다. 그렇지 않으면 반복문의 내용 {{수학 변수|S}}가 더 이상 {{수학 변수|t}}를 감소시킬 수 없고, 규칙의 전제가 거짓이 되기 때문이다. (이는 총 정확성을 나타내는 다양한 표기법 중 하나이다.)<ref group="note"> 호어의 원본 논문에서는 총 정확성에 관한 규칙을 제시하지 않았다 (p.579 논의 참조). 레이놀즈(Reynolds)의 교과서에는 다음과 같은 총 정확성 규칙이 있다: {{수학 변수|z}}가 {{수학 변수|P}}, {{수학 변수|B}}, {{수학 변수|S}}에서 자유 변수가 아닌 정수 변수이고, {{수학 변수|t}}가 정수 표현일 때,
<math>\dfrac{P \wedge B \rightarrow 0\leq t\quad ,\quad   [P \wedge B \wedge t=z] S [P \wedge t<z]}{[P] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [P \wedge \neg B]}</math>이다.</ref>

이전 절의 첫 번째 예시인

: <math>[x \leq 10]\texttt{while}\ x < 10\ \texttt{do}\ x:=x+1\ \texttt{done} [\neg x < 10 \wedge x \leq 10]</math>

에서는, 확장된 반복문 규칙을 사용해서 총 정확성을 증명할 수 있다.
{{수학 변수|D}}를 보통 순서를 가진 자연수 집합, 표현 {{수학 변수|t}}를 <math>10 - x</math>으로 놓고 반복문 규칙을 적용하여, 다음 목표를 얻는다.

: <math>[x \leq 10 \wedge x < 10 \wedge 10-x \geq 0 \wedge 10-x = z] x:= x+1 [x \leq 10 \wedge 10-x \geq 0 \wedge 10-x < z]</math>

거칠게 말하자면, 매 반복마다 '종료까지 남은 거리' <math>10-x</math>가 음수가 아닌 상태를 유지하며 줄어든다는 것을 증명하여야 한다. 이 감소 과정은 자연수의 감소 수열을 이루므로, 유한한 횟수의 반복 이후에 종료되어야 한다.

증명 목표는 다음과 같이 단순화될 수 있다.

: <math>[x < 10 \wedge 10-x = z]  x:=x+1  [x \leq 10 \wedge 10-x < z]</math>

이는 다음과 같이 증명할 수 있다.

* 할당 규칙을 통해 <math>[x+1 \leq 10 \wedge 10-x-1 < z]  x:=x+1  [x \leq 10 \wedge 10-x < z]</math>을 얻는다.
* 결과 규칙에 따라 <math>[x+1 \leq 10 \wedge 10-x-1 < z]</math>를 <math> [x < 10 \wedge 10-x = z]</math>으로 강화할 수 있다.

이전 절의 두 번째 예에서는 반복이 비어 있으므로 반복 내용에 의해 감소하는 표현 {{수학 변수|t}}를 찾을 수 없고, 따라서 종료를 증명할 수 없다.

== 같이 보기 ==
{{columns-list|* [[표명]]
* [[표시적 의미론]]
* [[규약에 따른 설계]]({{lang|en|Design by contract}})
* {{임시링크|동적 논리|en|Dynamic logic (modal logic)}}({{lang|en|Dynamic logic}})
* [[형식적 검증]]({{lang|en|Formal verification}})
* [[반복 불변량]]({{lang|en|loop invariant}})
* {{임시링크|술어변환의미론|en|Predicate transformer semantics}}({{lang|en|Predicate transformer semantics}})
* [[정적 프로그램 분석]]|colwidth=20em}}

== 각주 ==
{{각주|group=note}}

== 참고자료 ==
{{각주}}

== 읽을거리 ==
* Robert D. Tennent. ''[http://www.cs.queensu.ca/home/specsoft/ Specifying Software]'' (호어 논리에 대한 소개가 포함된 교과서, 2002년){{ISBN|0-521-00401-2}}

== 외부 링크 ==
* [https://web.archive.org/web/20071117054808/http://www.key-project.org/download/hoare/ KeY-Hoare] [[KeY]] 정리증명기를 기반으로 구축된 반자동 검증 시스템. 간단한 while 언어에 대한 호어 대수가 특징이다.
* [http://j-algo.binaervarianz.de/index.php?language=en j-Algo-modul 호어 대수] {{웹아카이브|url=https://web.archive.org/web/20110505192011/http://j-algo.binaervarianz.de/index.php?language=en}}  &#x2014; 알고리즘 시각화 프로그램 j-Algo의 호어 대수 시각화
{{전거 통제}}

[[분류:정적 프로그램 분석]]
[[분류:1969년 컴퓨팅]]
[[분류:컴퓨터 과학 내 논리]]