호어논리학

호어 논리학(Floyd –라고도 함)Hoare logic 또는 Hoare rules)은 컴퓨터 프로그램의 정확성에 대해 엄격하게 추론하기 위한 일련의 논리적 규칙을 가진 공식적인 시스템입니다.1969년 영국의 컴퓨터 과학자이자 논리학자인 토니 호어(Tony Hoare)에 의해 제안되었고, 호어와 다른 연구자들에 의해 개선되었습니다.^[1]그 독창적인 아이디어는 로버트 W의 작품에 의해 뿌려졌습니다. 플로이드는 비슷한 시스템을^[2] 플로우차트에 발표했습니다.

호어트리플

호아레 논리의 중심 특징은 호아레 트리플입니다.트리플은 코드 조각의 실행이 계산의 상태를 어떻게 변화시키는지를 설명합니다.호아레 트리플은 다음과 같은 형태입니다.

${\displaystyle \{P\}C\{Q\}$

여기서 $P{\displaystyle }$ ${\displaystyle P}$ 및$$ $Q{\displaystyle }$ ${\displaystyle Q}$은(는) 주장이고 $C{\displaystyle }$ ${\displaystyle C}$은(는) 명령입니다.^{[note 1]}${\displaystyle P}$ ${\displaystyle P}$는 전제 조건, Q ${\displaystyle Q}$는 사후 조건으로 명명됩니다. 전제 조건이 충족되면 명령을 실행하면 사후 조건이 성립됩니다.주장은 술어 논리에서 공식입니다.

호어 논리는 단순 명령형 프로그래밍 언어의 모든 구성 요소에 대한 공리와 추론 규칙을 제공합니다.Hoare의 원래 논문에서 간단한 언어에 대한 규칙 외에도, 그 이후 Hoare와 다른 많은 연구자들에 의해 다른 언어 구성에 대한 규칙이 개발되었습니다.동시성, 절차, 점프, 포인터에 대한 규칙이 있습니다.

부분정정 및 전정

표준 Hoare 논리를 사용하면 부분적인 정확도만 증명할 수 있습니다.전체 수정에는 종료도 추가로 필요하며, 이는 개별적으로 또는 While 규칙의 확장 버전을 사용하여 증명할 수 있습니다.^[3]따라서 호아레 트리플의 직관적 판독은 다음과 같습니다.$C{\displaystyle }$ ${\displaystyle C}$을(를) 실행하기 전에 $P{\displaystyle }$ ${\displaystyle P}$이(가) 상태를 유지할$$ 때마다$$이후에 $Q{\displaystyle }$ ${\displaystyle Q}$이(가) 유지되거나 $C{\displaystyle }$ ${\displaystyle C}$이(가) 종료되지 않습니다$$.후자의 경우 "후"가 없으므로 $Q{\displaystyle }$ ${\displaystyle$ Q$}$은(는) 임의의 문이 될 수 있습니다$$.실제로 $Q{\displaystyle }$ ${\displaystyle Q}$을(를) false로 선택하여 $C{\displaystyle }$ ${\displaystyle C}$이(가) 종료되지$$ 않음을 나타낼 수 있습니다.

여기와 이 글의 나머지 부분에서 "종료"는 넓은 의미에서 계산이 최종적으로 완료된다는 것을 의미합니다. 즉 무한 루프의 부재를 의미합니다. 프로그램을 조기에 중단하는 구현 제한 위반(예: 0으로 분할)의 부재를 의미하는 것은 아닙니다.1969년 논문에서 Hoare는 구현 제한 위반의 부재를 수반하는 더 좁은 종료 개념을 사용했으며, 주장을 구현 독립적으로 유지하기 때문에 더 넓은 종료 개념에 대한 선호를 표명했습니다.^[4]

위에서 인용한 공리와 규칙의 또 다른 단점은 프로그램이 성공적으로 종료되었다는 증거에 대한 근거를 제공하지 않는다는 것입니다.종료 실패는 무한 루프로 인해 발생할 수도 있고, 구현이 정의한 한계(예: 숫자 피연산자 범위, 스토리지 크기 또는 운영 체제 시간 제한) 위반으로 인해 발생할 수도 있습니다.따라서 "${\displaystyle }${ ${\displaystyle Q}$ ${\displaystyle \}}$ ${\displaystyle R}$ ${\displaystyle$ P$\{Q\}R$ 표기는 "프로그램이 성공적으로 종료되고 결과의 $속성$이 R ${\displaystyle R}$로 설명되는 경우"로 해석해야 합니다.$$ 이 공리들은 비종료 프로그램의 "결과"를 예측하는 데 사용될 수 없도록 꽤 쉽게 조정할 수 있지만 실제로는 이 공리를 사용합니다.이제 oms는 컴퓨터의 크기와 속도, 숫자의 범위, 오버플로 기술의 선택과 같은 많은 구현에 의존하는 기능에 대한 지식에 의존하게 됩니다.무한 루프를 피할 수 있다는 증거와는 별개로, 프로그램의 "조건부" 정확성을 증명하고 구현 한계를 위반하여 프로그램의 실행을 포기해야 하는 경우에는 구현에 의존하여 경고를 주는 것이 더 나을 수 있습니다.

규칙.

빈 문 공리 스키마

빈 문 규칙은 다음을 주장합니다.skip statement는 프로그램의 상태를 변경하지 않으므로 skip 전에 true로 유지되는 것은 나중에도 true로 유지됩니다.^{[note 2]}

${\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}$

할당 공리 스키마

할당 공리는 할당 후에 할당의 오른쪽에 대해 이전에 참이었던 모든 술어가 이제 변수에 대해 유지된다는 것을 나타냅니다.공식적으로 P를 변수 x가 자유인 주장이라고 합니다.그러면:

${\displaystyle {\dfrac {}{\{P[E/x]\}x:=E\{P\}}}"$

여기서 $P{\displaystyle }$[ ${\displaystyle E}$ /${\displaystyle x}$] ${\displaystyle P$[ E / x$]}$는 x의 각 자유 발생이 식 E로 대체된 주장 P를 나타냅니다$$.

할당 공리 체계는 $P{\displaystyle [E/x]}$ ${\displaystyle P[E/x]}$의 참값이 P의 할당 후 참값과 동일함을$$ 의미합니다.따라서 할당 전에는 ${\displaystyle \mathrm{할당}}$ 공리에 의해 P${\displaystyle }$[${\displaystyle E}$/ x ] {\displaystyle P$[E/x]}$이(가) 참이었고, 그 후에는 P가 참이 됩니다.반대로 할당 문 전에 $P{\displaystyle }$[${\displaystyle E}$ /${\displaystyle }$x${\displaystyle }$] ${\displaystyle$ P $[E/x]}$이(즉, ¬ P${\displaystyle }$[${\displaystyle E}$/ ${\displaystyle x]}$ ${\displaystyle \neg P[E/x]}$이(가) 참이면 나중에는 P가 거짓이어야 합니다.

유효한 삼중항의 예는 다음과 같습니다.

• ${\displaystyle \{x+1=43\}y:=x+1\{y=43\}$
• ${\displaystyle \{x+1\leq N\}x:=x+1\{x\leq N\}$

식에 의해 수정되지 않은 모든 전제 조건은 사후 조건으로 이월될 수 있습니다.첫 번째 예에서 $y$ := ${\displaystyle x}$+ ${\displaystyle 1}$ ${\displaystyle$y :=$x+1}$을(를) 할당해도 $x{\displaystyle }$+ ${\displaystyle 1}$ = ${\displaystyle 43}$ ${\displaystyle x+1$=$43}$이(가) 변경되지 않으므로 두 문 모두 후 조건에 나타날 수 있습니다$.$형식적으로, 이 결과는 P인 공리 스키마($$ = ${\displaystyle 43}$ ${\displaystyle$y=$43}$ 및 $x{\displaystyle }$+ ${\displaystyle 1}$ = ${\displaystyle 43}$ ${\displaystyle x+1$=$43})$를 적용함으로써 얻어지는데, 이를 $통해{\displaystyle }$P [ (${\displaystyle x}$+${\displaystyle }$${\displaystyle 1}$${\displaystyle }$) /${\displaystyle y}$ ]$${\$displaystyle$ P [ (x$$+$1)$ / $y]}$이($x$ ${\displaystyle +}$ 1 = ${\displaystyle 43}$ ${\displaystyle$ x$+1$=$43},$ x${\displaystyle }$+ ${\displaystyle 1}$ = ${\displaystyle 43}$ ${\displaystyle x+1$=$43})$로 단순화할 수 있습니다.${\displaystyle x+}$ ${\displaystyle 1}$ $=$ ${\displaystyle 43}$ ${\displaystyle$ = $43$

과제 공리 체계는 전제 조건을 찾기 위해서는 먼저 사후 조건을 취하고 과제의 왼쪽에서 발생하는 모든 것을 과제의 오른쪽으로 대체하라는 것과 같습니다.이 잘못된 사고 방식을 따라서 이를 거꾸로 하려고 하지 않도록 주의하십시오.$${${\displaystyle P\}}$ ${\displaystyle x}$ ${\displaystyle :}$= ${\displaystyle E}$ ${\displaystyle \{P}$[${\displaystyle E}$/ ${\displaystyle x}$]${\displaystyle }$}$${\$displaystyle \{P\}x:$$=E\{P[E/x$ 이 규칙은 다음과 같은 말도 안 되는 예로 이어집니다.

${\displaystyle \{x=5\}x:=3\{3=5\}$

언뜻 보기에는$${${\displaystyle P\}}$ ${\displaystyle x}$ :${\displaystyle }$= ${\displaystyle E}${${\displaystyle P}$ ∧ ${\displaystyle x}$ = ${\displaystyle E\}}$ ${\displaystyle \{P\}x:$$=E\{P\wedge x=$E$\backslash \}\};$ 다음과 같은 말도 안 되는 예로 이어집니다.

${\displaystyle \{x=5\}x:=x+1\{x=5\wedge x=x+1\}$

주어진 사후 조건 P가 전제 조건 $P{\displaystyle [E/x]}$ ${\displaystyle P[E/x]}$를 고유하게 결정하지만$,$ 그 역은 참이 아닙니다.예를 들어,

• ${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle y}$ ${\displaystyle \cdot }$ y ${\displaystyle \cdot }$ ${\displaystyle y}$ ${\displaystyle \le }$ ${\displaystyle 9}$ ${\displaystyle \}}$ ${\displaystyle x}$ :${\displaystyle =}$ ${\displaystyle y}$ ${\displaystyle \cdot y}$ { ${\displaystyle 0\le }$ ${\displaystyle x}$ ∧ ${\displaystyle x}$≤ $}$ {\$displaystyle$\{$0\leq$ y$\cd$ y$\cdoty\}$ : = $y\cdoty\{0\leq$ x$\leq 9$
• ${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle y}$ ${\displaystyle \cdot }$ y ${\displaystyle \cdot }$ ${\displaystyle y}$ ${\displaystyle \le }$ ${\displaystyle 9}$ ${\displaystyle \}}$ ${\displaystyle x}$ :${\displaystyle =}$ ${\displaystyle y}$ ${\displaystyle \cdot }$ ${\displaystyle y}${ ${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$ ${\displaystyle \wedge }$ ${\displaystyle y}$ ⋅ ${\displaystyle y}$ ${\displaystyle \le }$ ${\displaystyle 9}$ ${\displaystyle \}}$ ${\displaystyle \{0\leq y\cd$ : = $y\cdoty\{0\le$edge $y\cdoty\leq 9$
• ${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle y}$ ${\displaystyle \cdot }$ y ${\displaystyle \cdot }$ ${\displaystyle y}$ ${\displaystyle \le }$ ${\displaystyle 9}$ ${\displaystyle \}}$ ${\displaystyle x}$ :${\displaystyle =}$ ${\displaystyle y}$ ${\displaystyle \cdot }$ ${\displaystyle y}${ ${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle y}$ ${\displaystyle \cdot }$ ${\displaystyle y}$ ∧ ${\displaystyle x}$ ${\displaystyle \le }$ ${\displaystyle 9}$ ${\displaystyle \}}$ ${\displaystyle \{0\leq$ y$\cd$ : = $y\cdoty\{0\leq y\cd$edge $x\leq$ 9$\},$및
• ${\displaystyle \{0\leqy\cdoty\wedge y\cdoty\leq 9\}x:=y\cdoty\{0\leqy\cdoty\wedge y\cdoty\leq 9\}$

할당 공리 체계의 유효한 예입니다.

Hoare에서 제안한 할당 공리는 둘 이상의 이름이 동일한 저장 값을 참조할 수 있는 경우에는 적용되지 않습니다.예를들면,

${\displaystyle \{y=3\}x:=2\{y=3\}$

할당 공리 체계의 적절한 인스턴스$(\{{\displaystyle P}$ ${\displaystyle \}}$ ${\displaystyle$\{$P\}}$$$및 {${\displaystyle P}$[${\displaystyle 2}$ /${\displaystyle x}$ ]${\displaystyle \}}$ ${\displaystyle \{P[$2/x]\}) ${\$displaystyle \{P[$2/x]\}$가$${${\displaystyle y}$ = ${\displaystyle 3}$} {\$displaystyle \{y$ = $3\})$이더라도 x와 y가 동일한 변수(에일리어싱)를 참조하면 잘못된 것입니다.

구성규칙

스왑 코드 확인 중 보조 변수 없이
아래의 세 문장(2, 4, 6행)은 보조 변수 없이 변수 a와 b의 값을 교환합니다. Nr 코드 주장 1: ${\displaystyle \{a=A\wedge b=B\}$ 2: ${\displaystyle a:=a+b;}$ 3: ${\display style \{a-b=A\wedge b=B\}$ 4: ${\displaystyle b:=a-b;}$ 5: ${\displaystyle \{b=A\wedge a-b=B\}$ 6: ${\displaystyle a:=a-b}$ 7: ${\displaystyle \{b=A\wedge a=B\}$

Hoare의 구성 규칙은 순차적으로 실행되는 프로그램 S와 T에 적용되며, 여기서 S는 T보다 먼저 실행되고 $S{\displaystyle ;}$ ${\displaystyle T}$ ${\displaystyle S;T}$라고 쓰여집니다 $$(Q는 중간 조건이라고 불립니다).^[5]

${\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}}$

예를 들어, 다음과 같은 할당 공리의 두 가지 인스턴스를 생각해 보겠습니다.

${\displaystyle \{x+1=43\}y:=x+1\{y=43\}$

그리고.

${\displaystyle \{y=43\}z:=y\{z=43\}$

순서 규칙에 따라 다음과 같이 결론을 내립니다.

${\displaystyle \{x+1=43\}y:=x+1;z:=y\{z=43\}$

다른 예는 오른쪽 상자에 나와 있습니다.

조건부 규칙

${\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\}}}$

조건부 규칙은 그때와 다른 부분에 공통되는 후조건 Q도 if...endif 문장 전체의 후조건이라고 말합니다.^[6]그 다음 부분과 다른 부분에서, 부정되지 않은 조건 B를 각각 전제 조건 P에 추가할 수 있습니다.B 조건에는 부작용이 없어야 합니다.예는 다음 절에 나와 있습니다.

이 규칙은 호아레의 원래 출판물에는 포함되어 있지 않았습니다.^[1]그러나 진술 이후로

${\displaystyle {\texttt {if}}\B\{\texttt {then}}\S\{\texttt {else}}\T\{\texttt {endif}}$

일회성 루프 구성과 동일한 효과를 갖습니다.

${\displaystyle {\texttt {boole}}\ b:={\texttt {true};{\texttt {where}}\ B\wedge b\{\texttt {do}}\ S:={\texttt {done};b:={\texttt {true}};{\texttt {where}}\neg B\wedge b\{\texttt {do}}\ T;b:={\texttt {false}}\{\texttt {done}}$

조건부 규칙은 다른 Hoare 규칙에서 유도할 수 있습니다.비슷한 방식으로, 루프와 같은 다른 파생 프로그램 구성 요소에 대한 규칙은...Hoare의 원래 논문에서 규칙으로 프로그램을 변환하여 루프, 스위치, 브레이크, 계속을 줄일 수 있을 때까지.

결과규칙

${\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\quad ,\quad Q_{2}\quad ,\quad Q_{1}}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}}}}$

이 규칙은 사전 조건 ${\displaystyle {P2\mathrm{}}_{}}$ ${\$를 강화하고/또는 사후 조건 ${\displaystyle {Q2\mathrm{}}_{}}$ ${\$를 약화시킬 수 있습니다$.$ 이 규칙을 사용하면 다음 부분과 다른 부분에 대해 문자 그대로 동일한 사후 조건을 달성할 수 있습니다.

예를 들어, 의 증명.

${\displaystyle \{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}\}$

조건부 규칙을 적용할 필요가 있으며, 이를 증명해야 합니다.

< :$=$ + { ${\displaystyle \{0\leq$ x$\leq 15\}$x $edg$x:= $x+1\{0\leq x\leq 15\}$ 또는단순화됨

${\displaystyle \{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}$

그 다음에는, 그리고.

${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$ ${\displaystyle \le 15}$ ${\displaystyle \wedge }$ ${\displaystyle x}$ ≥ ${\displaystyle 15}$ ${\displaystyle \}}$ ${\displaystyle x}$ :$=$ 0${\displaystyle }${${\displaystyle 0}$≤ ${\displaystyle x}$≤ ${\displaystyle 15}$} ${\displaystyle \{0\leq x\leq 15\}$ : = $0\{0\leq x\leq 15\}$ 또는$$단순화

${\displaystyle \{x=15\}x:=0\{0\leq x\leq 15\}$

다른 쪽에 대해서는

그러나 그 다음 부분에 대한 할당 $규칙$은${\displaystyle }$P를 ${\displaystyle 0}$ ≤ x$≤ 15$ {\$displaystyle$0$\leq$ x\leq $15}$로 선택해야 합니다$.$ 따라서 규칙 적용으로 인해 산출됩니다.

${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$+ ${\displaystyle 1}$ ${\displaystyle \le }$ ${\displaystyle 15}$ ${\displaystyle \}}$x :$=$ ${\displaystyle \mathrm{x}}$+ ${\displaystyle 1}${${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$ ${\displaystyle \le }$ ${\displaystyle 15}$ ${\displaystyle \}}$ ${\displaystyle \{0\leq$ x$+1\leq 15$:= $x+1\{0\leq x\leq 15\},$논리적으로 다음과 같습니다.

< x :$=$ + 1 ${\displaystyle \{-1\leq$ x$<15\}$x := $x+1\{0\leq$ x$\leq 15\}.$

결과 규칙은 할당 규칙에서 얻은 전제 조건 < ${\displaystyle \{-1\leq$ x$<15\}$를 조건 규칙에 필요한{ x< ${\displaystyle \{0\leq x<15\}$로 강화하기 위해 필요합니다.

마찬가지로, 다른 부분의 경우 할당 규칙은

${\displaystyle \{}{\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle 15}$ ${\displaystyle \}}$x :$=$ 0${\displaystyle }${${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$ ${\displaystyle \le }$ ${\displaystyle 15}$ ${\displaystyle \}}$ ${\displaystyle \{0\leq 0\leq 15\$ x:=$0\{0\leq x\leq 15\} 또는$이와 동등한 값

${\displaystyle \{}{\displaystyle \mathtt{\text{true}}}$ ${\displaystyle \}x}$ :$=$ 0${\displaystyle }${${\displaystyle 0}$ ${\displaystyle \le }$ ${\displaystyle x}$ ${\displaystyle \le }$ ${\displaystyle 15}$ ${\displaystyle \}}$ ${\displaystyle \{\texttt {true}$:=$0\{0\leq x\leq 15$

따라서 ${\displaystyle {P1}_{}}$ ${\displaystyle P_{1}}$와 ${\displaystyle {P2}_{}}$ ${\displaystyle P_{2}$는 각각$$$\{{\displaystyle x}$=${\displaystyle 15\}}$ ${\displaystyle \{x$=$15\}}$와 {${\displaystyle \mathtt{\text{true}}\}}${\$displaystyle \{\texttt {true}\}$가 적용되어 전제 조건을 다시 강화해야 합니다.비공식적으로, 결과 규칙의 효과는$${${\displaystyle x}$= ${\displaystyle 15}$ ${\displaystyle \}}$ ${\displaystyle \{x$ = $15\}}$이(가) 다른 부분에 사용된 할당 규칙은 해당 정보를 필요로 하지 않기 때문에 다른 부분의 입구에서 알 수 있는 "forget"입니다.

통치하는 동안

${\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {where}}\B\{\texttt {do}}\S\{\texttt {done}\{\neg B\wedge P\}}}$

여기서 P는 루프 불변량이며, 이는 루프 본체 S에 의해 보존되어야 합니다. 루프가 끝난 후에도 이 불변량 P는 여전히 유지되며, ¬ ${\displaystyle B}$ ${\displaystyle \neg B}$가 루프를 종료하게 했음에 틀림없습니다.조건부 규칙에서와 같이 B는 부작용이 없어야 합니다.

예를 들어, 의 증명.

${\displaystyle \{x\leq 10\}{\texttt {where}}\ x<10\{\texttt {do}}\ x:=x+1\{\texttt {done}}\{\neg x<10\texttt 10\}$

그 동안은 증명해야 하는 규칙입니다.

< x :$=$ + { ${\displaystyle \{x\leq$x:= $x+1\{x\leq 10\}$ 또는단순화됨

< :$=$ + { ${\displaystyle \{x<10$:=$x+1\{x\leq 10$

할당 규칙에 의해 쉽게 얻을 수 있습니다.마지막으로, 후조건 ¬ <∧ ${\displaystyle \{\$${\displaystyle \mathrm{neg}}$ $x<10\$wedge x$\leq 10$${\displaystyle \backslash \}\}}$ ${\displaystyle \{x$=$10\}}$로 단순화할 수 있습니다$.$

다른 예를 들어, while 규칙을 사용하여 임의의 숫자 a의 정확한 제곱근 x를 계산하기 위해 다음과 같은 이상한 프로그램을 공식적으로 확인할 수 있습니다.

${\displaystyle \{\texttt {true}}\}{\texttt {while}}\x\cdot x\neq a\{\texttt {do}}\{\texttt {done}\x\cdot x=a\texttt {true}\}$

P가 참인 상태에서 while rule을 적용한 후 증명해야 합니다.

${\displaystyle \{}{\displaystyle \mathtt{\text{t}}r\mathtt{\text{ue}}}$ ${\displaystyle \wedge }$ ${\displaystyle x}$ ${\displaystyle \cdot }$ ${\displaystyle x}$ ≠ ${\displaystyle a}$ ${\displaystyle \}}$ ${\displaystyle \mathtt{\text{생략}}}${${\displaystyle \mathtt{\text{true}}}$}${\displaystyle \{\texttt {tru$ a$\}{\text$skip$}}\{\texttt {true$

건너뛰기 규칙과 결과 규칙에서 따르게 됩니다.

사실, 이상한 프로그램은 부분적으로 맞습니다: 만일 그것이 우연히 종료되었다면, x가 a의 제곱근 값을 포함하고 있었던 것이 확실합니다.다른 모든 경우에는 종료되지 않으므로 완전히 정확한 것은 아닙니다.

완전한 정확성을 위한 규칙이 있는 동안

위의 통상적인 규칙이 다음 규칙으로 대체된다면, Hoare 미적분학은 부분적인 정확성뿐만 아니라 전체적인 정확성, 즉 종결성을 증명하는 데에도 사용될 수 있습니다.일반적으로 여기서는 프로그램의 정확성에 대한 다른 개념을 나타내기 위해 곱슬곱슬한 괄호 대신 대괄호를 사용합니다.

${\displaystyle {\dfrac {<\\text{는 세트에 대한 기본 순서입니다}}\D\quad ,\quad [P\wedge B\wedge\in D\wedge get=z]S[P\wedget\in D\wedget<z]}{[P\wedget\in D]{\texttt {where}}\B\{\texttt {do}}\S\{\texttt {done}}[\neg B\wedget\in D]}}$

이 규칙에서, 루프 불변성을 유지하는 것 외에도, 각각의 반복 동안 일부 도메인 집합 D에서 잘 근거된 관계 <와 관련하여 값이 엄격하게 감소하는 루프 변형이라고 불리는 표현 t를 통해 종결을 증명합니다.<이(가) 기초가 잘 되어 있기 때문에, 엄격하게 감소하는 D의 구성원 체인은 유한한 길이만을 가질 수 있으므로 영원히 감소할 수 없습니다. (예를 들어, 일반적인 순서 <>는 양의 $정수{\displaystyle \mathbb{}}$ N ${\$에 기초하지만$,$ 정수 $Z{\displaystyle \mathbb{}}$ ${\$에도$,$ 양의 실수 $R{\displaystyle {\mathbb{}}^{}}$+ ${\$}에도 기초하지 않습니다.$hbb {R} ^{+};$이 모든 집합들은 계산적인 의미가 아니라 수학적인 의미를 갖으며, 특히 모든 집합들은 무한합니다.

루프 불변성 P가 주어졌을 때, 조건 B는 그것이 D의 최소 요소가 아니라는 것을 암시해야 합니다. 그렇지 않으면 체 S가 더 이상 감소할 수 없기 때문입니다. 즉, 규칙의 전제는 거짓이 될 것입니다.(이것은 완전 정확도를 위한 다양한 표기법 중 하나입니다.)

이전 섹션의 첫 번째 예제를 다시 시작하여 의 전체 수정 증명

${\displaystyle [x\leq 10]{\texttt {where}}\x<10\{\texttt {do}}\x:=x+1\{\texttt {done}}[\neg x<10\texttt x\leq 10]}$

반면에, 전체 정확도에 대한 규칙은 적용될 수 있는데, 예를 들어 D는 일반적인 순서를 가진 음이 아닌 정수이고, 식 t는 ${\displaystyle \mathrm{10}}$- x ${\displaystyle 10-x}$이며$,$ 이는 다음을 증명해야 합니다.

${\displaystyle [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]}$

비공식적으로 말하면, 우리는 ${\displaystyle \mathrm{거리}\mathrm{10}}$ -$$x {\$displaystyle 10-x}$가 항상 음이 아닌 상태로 유지되는 반면, 모든 루프 사이클에서 감소한다는$$ 것을 증명해야 합니다. 이 프로세스는 제한된 수의 사이클 동안만 진행될 수 있습니다.

이전 증명 목표는 다음과 같이 단순화할 수 있습니다.

< $=$ ]x := + [ ∧ - < z] ${\displaystyle [x$:=$x+1 [x\leq$edge $10-x<z$

다음과 같이 증명할 수 있습니다.

+ - -< z]x :$=$ + [ ∧ - < z] ${\displaystyle [x+1\leq$:=$x+1[x\leq$edge $10-x<z]}$는 할당 규칙에 의해 얻어지며,

+ - - < z] ${\displaystyle [x+1\leq$$edge$ $10-x-1<z]}$은(는) 결과 규칙에 의해[< ∧ $=$ {\$displaystyle [x$edge $0-x=z])$로 강화할 수 있습니다.

이전 섹션의 두 번째 예에 대해서는, 물론 빈 루프 본체에 의해 감소되는 표현 t를 찾을 수 없으므로, 종료는 증명될 수 없습니다.

참고 항목

메모들

참고문헌

추가열람

• 로버트 D.세입자.소프트웨어(2002년 작성된 호아레 논리학 개론을 포함한 교재) 지정 ISBN 0-521-00401-2

외부 링크

• KeY-Hoare는 KeY 정리 속담 위에 만들어진 반자동 검증 시스템입니다.간단한 언어를 위한 호아레 미적분이 특징입니다.
• j-Algo-modul Hoare 미적분학 — 알고리즘 시각화 프로그램 j-Algo에서 Hoare 미적분학의 시각화