호어 논리

호어 논리(영어: Hoare logic), 플로이드-호어 논리(영어: Floyd-Hoare logic) 또는 호어 규칙(영어: Hoare rules)은 컴퓨터 프로그램의 정확성(correctness)(영어판) 엄격하게 추론하기 위한 일련의 논리적 규칙을 갖춘 형식 체계이다. 1969년 영국의 컴퓨터 과학자이자 논리학자인 토니 호어는 호어 논리를 제안하였고, 이후 호어와 다른 연구자들이 호어 논리를 개선하였다.^[1] 원래 아이디어는 순서도에 대해 유사한 체계를 발표한 로버트 플로이드의 작업에서 비롯되었다.^[2]

호어 세 쌍[편집]

호어 논리의 핵심 특징은 호어 세 쌍(영어: Hoare triple)이다. 호어 세 쌍은 명령을 실행하는 것이 계산 상태를 어떻게 바꾸는지 설명한다. $P$ 와 $Q$ 가 표명(assertion)이고 $C$ 가 명령(command)일 때, 호어 세 쌍은 $\{P\}C\{Q\}$ 와 같은 형태이다.^{[note 1]} 이때 $P$ 는 전제 조건(precondition), $Q$ 는 사후 조건(postcondition)으로, 위의 호어 세 쌍은 전제 조건이 충족된 상태에서 명령을 실행하였을 때 사후 조건이 성립함을 나타낸다. 각 표명은 1차 논리의 논리식이다.

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

부분 정확성과 총 정확성[편집]

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

즉, 호어 논리는 프로그램의 부분 정확성(partial correctness)만을 검증한다. 총 정확성(total correctness)을 보이기 위해서는 명령이 종료(termination)하는지 추가로 검증해야 한다. 이는 별도의 방법을 사용하거나 반복문 규칙을 확장하여 증명할 수 있다.^[3]

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

추론 규칙[편집]

빈 명령 공리 도식[편집]

빈 명령 공리 도식(empty statement axiom schema)은 다음과 같다.^{[note 2]}

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

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

할당 공리 도식[편집]

할당 공리 도식(assignment axiom schema)은 다음과 같다.

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

변수 $x$ 를 자유 변수로 갖는 표명 $P$ 에 대해, $P[E/x]$ 는 $P$ 에서 자유롭게 나타나는 $x$ 를 각각 표현 $E$ 로 치환하여 얻은 표명을 나타낸다.

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

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

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

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

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

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

$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}$ ,
$\{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\}$

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

합성 규칙[편집]

보조 변수 없는 swap 명령 검증

아래의 세 명령(2, 4, 6행)은 변수 $a$ 와 $b$ 의 값을 보조 변수 없이 교환한다. 증명에서 $a$ 와 $b$ 의 초기값은 각각 상수 $A$ 와 $B$ 로 표시하였다. 증명은 7행부터 거꾸로 읽는 것이 가장 좋다. 예를 들어, 5행은 7행에서 $a$ (6행의 대상 표현식)를 $a-b$ (6행의 소스 표현식)으로 대체하여 얻는다. . $a-(a-b)=b$ (5행→3행), $a+b-b=a$ (3행→1행)와 같은 산술 표현 단순화가 암묵적으로 사용되었다.
번호	명령	표명
1:		$\{a=A\wedge b=B\}$
2:	$a:=a+b;$
3:		$\{a-b=A\wedge b=B\}$
4:	$b:=a-b;$
5:		$\{b=A\wedge a-b=B\}$
6:	$a:=a-b$
7:		$\{b=A\wedge a=B\}$

합성 규칙(rule of composition)은 다음과 같다.^[5]

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

프로그램 $S$ 가 실행된 이후 프로그램 $T$ 를 실행하는 (즉 $S$ , $T$ 를 순차적으로 실행하는) 프로그램을 $S;T$ 으로 표기한다. 이때 $Q$ 는 중간 조건(midcondition)이라고 부른다.

예를 들어, 할당 공리의 다음 두 가지 예시

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

,

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

에서, 합성 규칙을 적용하여

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

조건문 규칙(conditional rule)에서, then과 else 부분에 공통되는 사후 조건 $Q$ 가 전체 조건문 if...endif의 사후 조건이 된다.^[6] then과 else에서는 전제 조건에 각각 $B$ 와 $\neg B$ 를 추가할 수 있다. 조건 $B$ 에는 부작용이 없어야 한다.

조건문 규칙은 호어의 원본 논문에는 포함되어 있지 않다.^[1] 그러나

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

는 일회성 반복문인

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

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

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

결과 규칙[편집]

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

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

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

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

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

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

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

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

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

반복문 규칙[편집]

반복문 규칙(while rule)은 다음과 같다.

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

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

예를 들어,

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

는 반복문 규칙에 의해,

\{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}

, 또는 단순화하여

\{x<10\}x:=x+1\{x\leq 10\}

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

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

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

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

\{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}

$P$ 를 true로 놓아 반복문 규칙을 적용하여, 다음을 증명하면 된다.

\{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}

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

총 정확성과 반복문 규칙[편집]

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

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

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

반복 불변량 $P$ 가 주어졌을 때, 조건 $B$ 는 $t$ 가 $D$ 의 극소 원소가 아니라는 것을 이끌어내야 한다. 그렇지 않으면 반복문의 내용 $S$ 가 더 이상 $t$ 를 감소시킬 수 없고, 규칙의 전제가 거짓이 되기 때문이다. (이는 총 정확성을 나타내는 다양한 표기법 중 하나이다.)^{[note 3]}

이전 절의 첫 번째 예시인

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

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

[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]

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

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

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

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

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

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

같이 보기[편집]

표명
표시적 의미론
규약에 따른 설계(영어판)(Design by contract)
동적 논리(영어판)(Dynamic logic)
형식적 검증(Formal verification)
반복 불변량(영어판)(loop invariant)
술어변환의미론(영어판)(Predicate transformer semantics)
정적 프로그램 분석

각주[편집]

↑ 호어의 원래 논문에서는 " $\{P\}C\{Q\}$ " 대신 " $P\{C\}Q$ "이 사용되었다.
↑ 호어 규칙을 자연 연역 표현법으로 표현하였다. 예를 들어, ${\dfrac {\alpha ,\beta }{\phi }}$ 는 " $α$ 와 $β$ 가 성립한다면 $φ$ 가 성립한다"를 의미한다. $α$ , $β$ 는 추론 규칙의 전제(premise)이고, $φ$ 는 추론 규칙의 결론(conclusion)이다. 전제가 없는 추론 규칙을 공리(axiom)라고 하고, ${\dfrac {}{\quad \phi \quad }}$ 으로 표기한다.
↑ 호어의 원본 논문에서는 총 정확성에 관한 규칙을 제시하지 않았다 (p.579 논의 참조). 레이놀즈(Reynolds)의 교과서에는 다음과 같은 총 정확성 규칙이 있다: $z$ 가 $P$ , $B$ , $S$ 에서 자유 변수가 아닌 정수 변수이고, $t$ 가 정수 표현일 때, ${\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]}}$ 이다.

참고자료[편집]

↑ ^가 ^나 Hoare, C. A. R. (October 1969). “An axiomatic basis for computer programming”. 《Communications of the ACM》 12 (10): 576–580. doi:10.1145/363235.363259.
↑ Floyd, R. W. (1967). “Assigning meanings to program” (PDF). 《Proceedings of the American Mathematical Society Symposia on Applied Mathematics》 19: 19–31.
↑ John C. Reynolds (2009). 《Theories of Programming Languages》. Cambridge University Press. ) Here: Sect. 3.4, p. 64.
↑ Hoare (1969), p.578-579
↑ Huth, Michael; Ryan, Mark (2004년 8월 26일). 《Logic in Computer Science》 seco판. CUP. 276쪽. ISBN 978-0521543101.
↑ Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (December 2019). “Fifty years of Hoare's logic”. 《Formal Aspects of Computing》 31 (6): 759. doi:10.1007/s00165-019-00501-3.

읽을거리[편집]

Robert D. Tennent. Specifying Software (호어 논리에 대한 소개가 포함된 교과서, 2002년)ISBN 0-521-00401-2

외부 링크[편집]

KeY-Hoare KeY 정리증명기를 기반으로 구축된 반자동 검증 시스템. 간단한 while 언어에 대한 호어 대수가 특징이다.
j-Algo-modul 호어 대수 Archived 2011년 5월 5일 - 웨이백 머신 — 알고리즘 시각화 프로그램 j-Algo의 호어 대수 시각화

[3] 호어의 원래 논문에서는 " $\{P\}C\{Q\}$ " 대신 " $P\{C\}Q$ "이 사용되었다.

[6] 호어 규칙을 자연 연역 표현법으로 표현하였다. 예를 들어, ${\dfrac {\alpha ,\beta }{\phi }}$ 는 " $α$ 와 $β$ 가 성립한다면 $φ$ 가 성립한다"를 의미한다. $α$ , $β$ 는 추론 규칙의 전제(premise)이고, $φ$ 는 추론 규칙의 결론(conclusion)이다. 전제가 없는 추론 규칙을 공리(axiom)라고 하고, ${\dfrac {}{\quad \phi \quad }}$ 으로 표기한다.

[9] 호어의 원본 논문에서는 총 정확성에 관한 규칙을 제시하지 않았다 (p.579 논의 참조). 레이놀즈(Reynolds)의 교과서에는 다음과 같은 총 정확성 규칙이 있다: $z$ 가 $P$ , $B$ , $S$ 에서 자유 변수가 아닌 정수 변수이고, $t$ 가 정수 표현일 때, ${\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]}}$ 이다.

[hoare-1] 가 ^나 Hoare, C. A. R. (October 1969). “An axiomatic basis for computer programming”. 《Communications of the ACM》 12 (10): 576–580. doi:10.1145/363235.363259.

[2] Floyd, R. W. (1967). “Assigning meanings to program” (PDF). 《Proceedings of the American Mathematical Society Symposia on Applied Mathematics》 19: 19–31.

[Reynolds.2009-4] John C. Reynolds (2009). 《Theories of Programming Languages》. Cambridge University Press. ) Here: Sect. 3.4, p. 64.

[5] Hoare (1969), p.578-579

[7] Huth, Michael; Ryan, Mark (2004년 8월 26일). 《Logic in Computer Science》 seco판. CUP. 276쪽. ISBN 978-0521543101.

[8] Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (December 2019). “Fifty years of Hoare's logic”. 《Formal Aspects of Computing》 31 (6): 759. doi:10.1007/s00165-019-00501-3.

[1]

[2]

[note 1]

[3]

[4]

[note 2]

[5]

[6]

[note 3]