호어 논리

틀:위키데이터 속성 추적 호어 논리(틀:Llang), 플로이드-호어 논리(틀:Llang) 또는 호어 규칙(틀:Llang)은 틀:임시 링크 엄격하게 추론하기 위한 일련의 논리적 규칙을 갖춘 형식 체계이다. 1969년 영국의 컴퓨터 과학자이자 논리학자인 토니 호어는 호어 논리를 제안하였고, 이후 호어와 다른 연구자들이 호어 논리를 개선하였다. 원래 아이디어는 순서도에 대해 유사한 체계를 발표한 로버트 플로이드의 작업에서 비롯되었다.

호어 세 쌍

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

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

부분 정확성과 총 정확성

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

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

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

추론 규칙

빈 명령 공리 도식

빈 명령 공리 도식(틀:Lang)은 다음과 같다.

$\frac{}{\{P\}\mathtt{\text{skip}}\{P\}}$

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

할당 공리 도식

할당 공리 도식(틀:Lang)은 다음과 같다.

$\frac{}{\{P[E/x]\}x:=E\{P\}}$

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

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

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

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

치환을 통해 바뀌지 않은 전제조건은 모두 사후조건으로 넘어갈 수 있다. 첫 번째 예에서는 할당 $y:=x+1$이후에도 $x+1=43$이라는 사실은 변하지 않으므로 표명 $x+1=43$은 사후 조건에 나타날 수 있다. 엄밀하게는, 틀:수학 변수를 "$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[E/x]$을 유일하게 결정하는 반면, 역은 성립하지 않는다. 다음 호어 세 쌍들은 모두 할당 공리 도식의 유효한 예시이고 같은 전제 조건을 가지고 있지만 서로 다른 사후 조건을 갖는다.

• $\{0\le y\cdot y\wedge y\cdot y\le 9\}x:=y\cdot y\{0\le x\wedge x\le 9\}$ ,
• $\{0\le y\cdot y\wedge y\cdot y\le 9\}x:=y\cdot y\{0\le x\wedge y\cdot y\le 9\}$,
• $\{0\le y\cdot y\wedge y\cdot y\le 9\}x:=y\cdot y\{0\le y\cdot y\wedge x\le 9\}$,
• $\{0\le y\cdot y\wedge y\cdot y\le 9\}x:=y\cdot y\{0\le y\cdot y\wedge y\cdot y\le 9\}$

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

합성 규칙

보조 변수 없는 swap 명령 검증

아래의 세 명령(2, 4, 6행)은 변수 틀:수학 변수와 틀:수학 변수의 값을 보조 변수 없이 교환한다. 증명에서 틀:수학 변수와 틀:수학 변수의 초기값은 각각 상수 틀:수학 변수와 틀:수학 변수로 표시하였다. 증명은 7행부터 거꾸로 읽는 것이 가장 좋다. 예를 들어, 5행은 7행에서 틀:수학 변수 (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\}$

합성 규칙(틀:Lang)은 다음과 같다.

$\frac{\{P\}S\{Q\},\{Q\}T\{R\}}{\{P\}S;T\{R\}}$

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

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

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

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

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

와 같은 결론을 얻을 수 있다.

조건문 규칙

$\frac{\{B\wedge P\}S\{Q\},\{\mathrm{\neg }B\wedge P\}T\{Q\}}{\{P\}\mathtt{\text{if}}B\mathtt{\text{then}}S\mathtt{\text{else}}T\mathtt{\text{endif}}\{Q\}}$

조건문 규칙(틀:Lang)에서, 틀:모노과 틀:모노 부분에 공통되는 사후 조건 틀:수학 변수가 전체 조건문 틀:모노의 사후 조건이 된다. 틀:모노과 틀:모노에서는 전제 조건에 각각 틀:수학 변수와 $\mathrm{\neg }B$를 추가할 수 있다. 조건 틀:수학 변수에는 부작용이 없어야 한다.

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

$\mathtt{\text{if}}B\mathtt{\text{then}}S\mathtt{\text{else}}T\mathtt{\text{endif}}$

는 일회성 반복문인

$\mathtt{\text{bool}}b:=\mathtt{\text{true}};\mathtt{\text{while}}B\wedge b\mathtt{\text{do}}S;b:=\mathtt{\text{false}}\mathtt{\text{done}};b:=\mathtt{\text{true}};\mathtt{\text{while}}\mathrm{\neg }B\wedge b\mathtt{\text{do}}T;b:=\mathtt{\text{false}}\mathtt{\text{done}}$

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

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

결과 규칙

$\frac{P_1\to P_2,\{P_2\}S\{Q_2\},Q_2\to Q_1}{\{P_1\}S\{Q_1\}}$

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

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

$\{0\le x\le 15\}\mathtt{\text{if}}x<15\mathtt{\text{then}}x:=x+1\mathtt{\text{else}}x:=0\mathtt{\text{endif}}\{0\le x\le 15\}$

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

• 틀:모노에 해당하는 $\{0\le x\le 15\wedge x<15\}x:=x+1\{0\le x\le 15\}$, 또는 단순화하여 $\{0\le x<15\}x:=x+1\{0\le x\le 15\}$를 증명하여야 한다.
• 틀:모노에 해당하는 $\{0\le x\le 15\wedge x\ge 15\}x:=0\{0\le x\le 15\}$, 또는 단순화하여 $\{x=15\}x:=0\{0\le x\le 15\}$를 증명하여야 한다.

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

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

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

반복문 규칙

반복문 규칙(틀:Lang)은 다음과 같다.

$\frac{\{P\wedge B\}S\{P\}}{\{P\}\mathtt{\text{while}}B\mathtt{\text{do}}S\mathtt{\text{done}}\{\mathrm{\neg }B\wedge P\}}$

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

예를 들어,

$\{x\le 10\}\mathtt{\text{while}}x<10\mathtt{\text{do}}x:=x+1\mathtt{\text{done}}\{\mathrm{\neg }x<10\wedge x\le 10\}$

는 반복문 규칙에 의해,

$\{x\le 10\wedge x<10\}x:=x+1\{x\le 10\}$, 또는 단순화하여 $\{x<10\}x:=x+1\{x\le 10\}$

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

$\{x\le 10\}\mathtt{\text{while}}x<10\mathtt{\text{do}}x:=x+1\mathtt{\text{done}}\{x=10\}$

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

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

$\{\mathtt{\text{true}}\}\mathtt{\text{while}}x\cdot x\ne a\mathtt{\text{do}}\mathtt{\text{skip}}\mathtt{\text{done}}\{x\cdot x=a\wedge \mathtt{\text{true}}\}$

틀:수학 변수를 틀:모노로 놓아 반복문 규칙을 적용하여, 다음을 증명하면 된다.

$\{\mathtt{\text{true}}\wedge x\cdot x\ne a\}\mathtt{\text{skip}}\{\mathtt{\text{true}}\}$

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

총 정확성과 반복문 규칙

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

$\frac{<\text{is a well-founded ordering on the set}D,[P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]\mathtt{\text{while}}B\mathtt{\text{do}}S\mathtt{\text{done}}[\mathrm{\neg }B\wedge P\wedge t\in D]}$

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

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

이전 절의 첫 번째 예시인

$[x\le 10]\mathtt{\text{while}}x<10\mathtt{\text{do}}x:=x+1\mathtt{\text{done}}[\mathrm{\neg }x<10\wedge x\le 10]$

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

$[x\le 10\wedge x<10\wedge 10-x\ge 0\wedge 10-x=z]x:=x+1[x\le 10\wedge 10-x\ge 0\wedge 10-x<z]$

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

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

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

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

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

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

읽을거리

• Robert D. Tennent. Specifying Software (호어 논리에 대한 소개가 포함된 교과서, 2002년)틀:ISBN

외부 링크

• KeY-Hoare KeY 정리증명기를 기반으로 구축된 반자동 검증 시스템. 간단한 while 언어에 대한 호어 대수가 특징이다.
• j-Algo-modul 호어 대수 틀:웹아카이브 — 알고리즘 시각화 프로그램 j-Algo의 호어 대수 시각화