호어 논리

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

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

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

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

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

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

## 추론 규칙

### 빈 명령 공리 도식
**[[NOP (코드)|빈 명령]] 공리 도식**()은 다음과 같다.

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

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

### 할당 공리 도식
**할당 공리 도식**()은 다음과 같다.

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

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

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

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

:* \{ 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은 사후 조건에 나타날 수 있다. 엄밀하게는, 를 "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 \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\}으로 놓아서 얻을 수 있으므로 할당 공리 도식의 유효한 예시이다. 하지만, 와 가 동일한 변수를 참조하는 경우(앨리어싱) 이는 올바르지 않다.

### 합성 규칙

**합성 규칙**()은 다음과 같다.

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

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

예를 들어, 할당 공리의 다음 두 가지 예시
: \{ 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\}}

**조건문 규칙**()에서, 과  부분에 공통되는 사후 조건 가 전체 조건문 의 사후 조건이 된다. 과 에서는 전제 조건에 각각 와  \neg B를 추가할 수 있다. 조건 에는 부작용이 없어야 한다.

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

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

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

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

### 결과 규칙

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

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

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

: \{0 \leq x \leq 15 \}\texttt{if}\ x

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

* 에 해당하는 \{0 \leq x \leq 15 \wedge x , 또는 단순화하여 \{0 \leq x 를 증명하여야 한다.
* 에 해당하는 \{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 \le x \le 15로 두어 할당 공리 도식을 적용하면 \{0 \leq x+1 \leq 15\}  x:=x+1  \{0 \leq x \leq 15\}, 또는 단순화하여 \{-1 \leq x 를 얻는다. 이 호어 세 쌍의 전제는 \{0 \leq x 보다 약하므로, 결과 규칙을 적용하여 \{0 \leq x 을 이끌어 내야 한다.

마찬가지로, 할당 공리 도식을 적용하면 \{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 \}를 증명하기 위해서는 그만큼 강한 정보가 필요하지 않기 때문이다.

### 반복문 규칙
**반복문 규칙**()은 다음과 같다.

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

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

예를 들어,

: \{x \leq 10\} \texttt{while}\ x

는 반복문 규칙에 의해,

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

: \{x \leq 10\} \texttt{while}\ x

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

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

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

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

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

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

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

: \dfrac{

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

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

이전 절의 첫 번째 예시인

: [x \leq 10]\texttt{while}\ x 

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

: [x \leq 10 \wedge x 

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

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

: [x 

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

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

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

## 같이 보기

## 각주

## 참고자료

## 읽을거리
* Robert D. Tennent. *[http://www.cs.queensu.ca/home/specsoft/ Specifying Software]* (호어 논리에 대한 소개가 포함된 교과서, 2002년)

## 외부 링크
* KeY-Hoare KeY 정리증명기를 기반으로 구축된 반자동 검증 시스템. 간단한 while 언어에 대한 호어 대수가 특징이다.
* j-Algo-modul 호어 대수   &#x2014; 알고리즘 시각화 프로그램 j-Algo의 호어 대수 시각화

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