호어 논리와 프로그램 검증(Hoare logic and program verification)

이진 탐색⁠(binary search)⁠ 페이지는 이진 탐색이 '간단해 보여도 정확하게 짜기는 의외로 까다롭다'고 말합니다. 그렇다면 제대로 짰는지는 어떻게 알까요? 시험해 보는 방법은 넣어 본 입력에 대해서만 답합니다. 길이 16인 배열 하나에 찾는 값을 바꿔 가며 넣어 보아도, 길이가 다른 배열과 다른 값들은 끝없이 남습니다. 데이크스트라가 1970년 「구조적 프로그래밍⁠(structured programming)⁠에 관한 노트」에 적은 대로, 시험은 오류가 있음을 보일 수는 있어도 없음을 보일 수는 없습니다. 남은 길은 증명입니다. 모든 입력에 대해 한꺼번에, 프로그램의 글자만 보고.

생각의 싹은 일찍 나왔습니다. 1949년 튜링은 짧은 발표 「큰 루틴 확인하기」에서 프로그램의 몇 곳에 '여기서는 이것이 참'이라는 단언을 붙이고, 끝남은 줄어드는 양으로 보이는 방법을 선보였습니다. 이 발표는 오래 잊혔고, 1967년 미국의 로버트 플로이드가 순서도의 화살표마다 조건을 붙여 프로그램의 뜻을 정하면서 생각이 다시 나왔습니다. 1969년 영국의 토니 호어는 이것을 프로그램 글자 위의 논리로 바꾸었습니다. $\{P\}\;C\;\{Q\}$는 '조건 P가 참인 상태에서 C를 실행하기 시작해 C가 끝나면, 끝난 상태에서 Q가 참이다'라는 주장이고, 호어 삼중⁠(Hoare triple)⁠이라 부릅니다. P를 전조건⁠(precondition)⁠, Q를 후조건⁠(postcondition)⁠이라 합니다. 이 주장은 C가 끝나지 않는 경우에 대해 아무것도 말하지 않습니다. 이것을 부분 정확성이라 하고, 끝남까지 보장하는 주장을 전체 정확성⁠(total correctness)⁠이라 해서 $[P]\;C\;[Q]$로 적기도 합니다.

규칙은 대입, 이어 붙이기, 조건문, 반복문 같은 문법 요소마다 하나씩 있고, 여기에 문법과 상관없이 조건을 바꿔 끼우는 결과 규칙이 더해집니다. 대입, 이어 붙이기, 결과 규칙은 이렇습니다.

$$\{Q[x := E]\}\; x := E\; \{Q\} \qquad \dfrac{\{P\}\,C_1\,\{R\} \quad \{R\}\,C_2\,\{Q\}}{\{P\}\;C_1;\,C_2\;\{Q\}} \qquad \dfrac{P \Rightarrow P' \quad \{P'\}\,C\,\{Q'\} \quad Q' \Rightarrow Q}{\{P\}\;C\;\{Q\}}$$

대입 규칙은 거꾸로 읽힙니다. $x := x + 1$ 뒤에 $x \gt 0$이 참이려면, 앞에서는 Q의 x 자리에 x + 1을 넣은 $x + 1 \gt 0$, 정수라면 $x \ge 0$이 참이어야 합니다. 앞에서 뒤로 가는 규칙은 훨씬 번거롭습니다. $x := x + 1$ 뒤에 무엇이 참인지 말하려면, 덮어써서 사라진 이전 값에 새 이름 $x_0$을 붙여 '$x = x_0 + 1$이고 $x_0$에 대해 P가 성립하는 $x_0$이 있다'고 적어야 하기 때문입니다. 이어 붙이기 규칙은 가운데 조건 R로 두 조각을 잇고, 결과 규칙은 전조건을 강하게(더 좁게), 후조건을 약하게(더 넓게) 바꿔도 된다고 말합니다. 조건문은 두 갈래에 b와 ¬b를 각각 더해 따집니다.

핵심은 반복문의 규칙입니다(위의 식). 반복 조건 b가 참일 때 몸통 C를 한 번 실행해도 깨지지 않는 조건 I, 곧 반복 불변식⁠(loop invariant)⁠을 찾으면, 반복이 끝났을 때 I와 ¬b가 함께 성립합니다. 규칙이 옳은 이유는 수학적 귀납법⁠(mathematical induction)⁠입니다. 0바퀴 뒤에 I가 참이고(처음에 참), k바퀴 뒤에 참이면 k + 1바퀴 뒤에도 참이니(몸통이 지킴), 몇 바퀴 뒤에 끝나든 I는 참입니다. 끝남은 따로 보여야 합니다. 상태로 정해지는 정수 V가 불변식 아래에서 늘 0 이상이고 한 바퀴마다 엄격히 줄어들면, 반복은 V의 처음 값보다 많이 돌 수 없습니다. 이런 V를 변량(종료 측도⁠(measure)⁠)이라 합니다. 음이 아닌 정수가 끝없이 줄어들 수는 없다는 사실은 귀납법의 다른 얼굴(정렬 원리⁠, well-ordering principle⁠)입니다.

이진 탐색으로 해 봅시다. 정렬된 배열 $a[0], \dots, a[n-1]$에서 t 이상인 첫 칸을 찾는 판입니다. t가 배열에 있다면 바로 그 칸에 있습니다. 불변식은 세 조각입니다.

$$I:\quad 0 \le lo \le hi \le n, \qquad a[j] \lt t \;\;(j \lt lo), \qquad a[j] \ge t \;\;(j \ge hi)$$

그림에서 lo 왼쪽의 파란 칸은 't보다 작다고 이미 확인된 곳', hi부터 오른쪽의 청록 칸은 't 이상이라고 확인된 곳입니다. 가운데 칸만 아직 모릅니다. 변량은 모르는 칸의 개수 $hi - lo$입니다. 찾는 값 t = , 프로그램:

증명은 네 가지 확인으로 끝납니다. (1) 처음: lo = 0, hi = n이면 I가 참입니다. $j \lt 0$인 칸도 $j \ge n$인 칸도 없으니, 둘째와 셋째 조건은 확인할 것이 없어 참입니다. (2) 보존: $a[mid] \lt t$이면, a가 정렬되어 있으므로 $j \le mid$인 모든 칸이 t보다 작고, 그래서 $lo := mid + 1$ 뒤에도 I가 참입니다. 다른 갈래도 같은 방식입니다. (3) 끝: 반복이 끝나면 $lo \ge hi$이고 I에서 $lo \le hi$이니 lo = hi입니다. 그러면 lo 왼쪽은 모두 t보다 작고 lo부터는 모두 t 이상이므로, lo가 t 이상인 첫 칸입니다. (4) 끝남: $lo \lt hi$일 때 $lo \le mid \lt hi$이므로, 어느 갈래로 가든 $hi - lo$가 적어도 1 줄어듭니다. 각 확인은 배열의 길이와 상관없는 짧은 산수이고, 이 네 줄이 길이가 16이든 10억이든, t가 무엇이든 성립한다는 증명입니다.

틀린 판 두 가지를 골라 보세요. 'lo := mid'로 쓰면 불변식은 지켜지지만 변량이 줄지 않는 순간이 옵니다. $hi - lo = 1$이면 mid = lo라서 lo := mid가 아무것도 바꾸지 않고, 프로그램은 영원히 돕니다(t = 30이면 네 바퀴 뒤에 hi − lo = 1이 되고, 다섯째 바퀴부터 제자리를 돕니다). 'hi := mid − 1'로 쓰면 반대로 끝남은 지켜지지만 불변식이 깨집니다. $a[mid] \ge t$라는 사실은 mid − 1번 칸에 대해 아무것도 말하지 않기 때문입니다. 부분 정확성⁠(partial correctness)⁠과 끝남은 서로 다른 증명이라는 것이 여기서 보입니다. 이진 탐색 페이지의 (lo + hi)/2 넘침 오류는 또 다른 종류입니다. 수학의 정수 대신 크기가 정해진 기계의 정수를 쓰기 때문에 생기므로, 식 E를 계산해도 넘치지 않는다는 조건까지 규칙에 넣어야 잡힙니다.

1975년 데이크스트라는 방향을 바꿨습니다. 후조건 Q와 프로그램 C가 주어지면, C가 반드시 끝나고 끝난 뒤 Q가 참이 되는 시작 상태 전체를 나타내는 조건, 곧 최약 전조건 wp(C, Q)를 계산하자는 것입니다. 대입은 $\mathrm{wp}(x := E,\; Q) = Q[x := E]$, 이어 붙이기는 $\mathrm{wp}(C_1; C_2,\; Q) = \mathrm{wp}(C_1,\; \mathrm{wp}(C_2, Q))$입니다. 예를 들어

$$\mathrm{wp}(x := x + 1;\; y := 2x,\;\; y \gt 10) \;=\; \mathrm{wp}(x := x + 1,\;\; 2x \gt 10) \;=\; \big(2(x + 1) \gt 10\big) \;=\; (x \gt 4).$$

프로그램은 후조건을 전조건으로 바꾸는 함수, 곧 술어 변환기⁠(predicate transformer)⁠가 됩니다. $[P]\;C\;[Q]$는 $P \Rightarrow \mathrm{wp}(C, Q)$와 같으니, 증명의 상당 부분이 계산으로 바뀝니다. 데이크스트라는 이것으로 프로그램을 다 짠 뒤에 검증하지 말고 명세에서 프로그램을 이끌어 내자고 주장했고, 1976년 책 『프로그래밍의 규율』에서 그 방법을 보였습니다.

끝남을 따지지 않는 판인 최약 자유 전조건⁠(weakest liberal precondition)⁠ wlp(C, Q)는 'C가 끝난다면 반드시 Q가 참'인 시작 상태의 조건입니다. 이것이 실행과 짝을 이룹니다. 시작 상태의 집합⁠(set)⁠ P에서 C를 실행해 닿을 수 있는 끝 상태를 모두 모은 것을 최강 후조건 sp(C, P)라 하면

$$\mathrm{sp}(C, P) \subseteq Q \;\iff\; P \subseteq \mathrm{wlp}(C, Q)$$

입니다. 양쪽 모두 {P} C {Q}, 곧 'P에서 출발해 끝나는 모든 실행이 Q에서 끝난다'는 말이기 때문입니다. 순서 사이의 이런 짝이 갈루아 연결이고, 수반 함자⁠(adjoint functor)⁠ 페이지에서 본 '∃ ⊣ 역상 ⊣ ∀'와 같은 모양입니다. sp는 '어떤 실행이 그리로 가는가'(∃)를, wlp는 '모든 실행이 그리로 가는가'(∀)를 묻습니다. 아래 점을 눌러 P를, 위 점을 눌러 Q를 바꿔 보세요. 프로그램:

갈루아 연결에서 공짜로 따라 나오는 것이 있습니다. 오른쪽 짝은 '그리고'를 보존하므로 $\mathrm{wlp}(C, Q_1 \land Q_2) = \mathrm{wlp}(C, Q_1) \land \mathrm{wlp}(C, Q_2)$이고, 왼쪽 짝은 '또는'을 보존하므로 $\mathrm{sp}(C, P_1 \lor P_2) = \mathrm{sp}(C, P_1) \lor \mathrm{sp}(C, P_2)$입니다. 데이크스트라가 술어 변환기가 지켜야 할 '건강 조건'으로 내세운 성질 가운데 하나가 이 '그리고'의 보존입니다. 끝나지 않는 상태가 있는 프로그램을 고르면 wlp와 wp의 차이도 보입니다. 어떤 실행도 끝나지 않는 시작 상태는 어떤 Q에 대해서도 wlp(Q)에 들어가지만 wp(Q)에는 들어가지 않습니다. '끝난다면'이 공허하게 참이기 때문입니다. 반복문의 wp는 영역 이론⁠(domain theory)⁠의 최소 고정점입니다. $X_0 = \lnot b \land Q$에서 시작해 $X_{k+1} = X_0 \lor (b \land \mathrm{wp}(C, X_k))$를 쌓으면 $X_k$는 'k바퀴 안에 끝나며 Q'이고, 이것들을 모두 '또는'으로 모은 것이 wp(while b do C, Q)입니다. 이 등식이 성립하려면, 곧 모든 k에 대한 '또는'만으로 최소 고정점⁠(least fixed point)⁠에 닿으려면 wp(C, ·)가 연속이어야 합니다. 데이크스트라는 한 상태에서 갈 수 있는 곳이 유한할 때(유한 비결정성) 이것이 성립함을 지적했습니다. 갈 수 있는 곳이 무한히 많으면 반드시 끝나지만 몇 바퀴 안에 끝난다고 미리 묶을 수 없는 상태가 생기고, 그런 상태는 어느 $X_k$에도 들지 않습니다.

한계도 분명합니다. 모든 프로그램의 부분 정확성을 판정하는 알고리즘⁠(algorithm)⁠은 없습니다. {참} C {거짓}은 'C는 어떤 상태에서 시작해도 끝나지 않는다'는 뜻이라, 그런 알고리즘은 정지 문제⁠(halting problem)⁠를 풀어 버리기 때문입니다. 그래서 불변식을 기계가 늘 알아서 찾아 줄 수는 없고, 1978년 스티븐 쿡이 보인 (부분 정확성에 대한) 완전성도 '상대적'입니다. 조건을 적는 언어가 충분히 표현력이 있고 그 언어의 참인 문장을 모두 안다고 치면, 참인 삼중은 모두 규칙으로 증명됩니다. 실제 도구는 분업을 합니다. 사람이 불변식과 변량을 적고, 기계가 나머지 검증 조건(위의 네 확인 같은 논리식)을 자동 증명기로 확인합니다. 2009년 무렵 나온 언어 다프니(Dafny)에서는 반복문 옆에 invariant와 decreases를 적습니다. 포인터와 공유 메모리는 2001–2002년 존 레이놀즈, 피터 오헌 등이 내놓은 분리 논리⁠(separation logic)⁠로 다룹니다. 분리 논리의 '분리된 그리고' $P \ast Q$는 'P와 Q가 서로 겹치지 않는 메모리 조각에서 각각 성립한다'는 뜻으로, 선형 논리⁠(linear logic)⁠의 ⊗처럼 자원을 나눠 쓰는 연결사입니다. 논리적 바탕은 선형 논리 자체가 아니라, 오헌과 데이비드 파임이 만든 가까운 친척인 BI 논리입니다.

흔한 오해 둘. 증명된 프로그램도 명세가 틀리면 틀립니다. '정렬한다'를 '출력이 정렬되어 있다'로만 적으면 빈 배열을 돌려주는 프로그램도 증명됩니다. 출력이 입력을 재배열한 것이라는 조건이 빠졌기 때문입니다. 호어 논리⁠(Hoare logic)⁠는 C가 명세를 지키는지 확인할 뿐, 명세가 원하는 것인지는 확인하지 않습니다. 또 불변식은 '언제나 참인 조건'이 아니라 반복 조건을 검사하는 순간마다 참인 조건입니다. 몸통을 실행하는 도중에는 잠깐 깨져도 됩니다. 배열의 합을 구하는 몸통 s := s + a[i]; i := i + 1의 불변식 $s = a[0] + \cdots + a[i-1]$은 첫 줄을 실행한 직후에는 (a[i]가 0이 아닌 한) 거짓이지만, 둘째 줄까지 마치면 다시 참입니다.

이어지는 곳. 여기서 증명한 프로그램은 이진 탐색이고, 반복문 규칙의 정당성과 변량의 논리는 수학적 귀납법에서 옵니다. 이 논리를 세운 사람들의 이야기는 토니 호어와 에츠허르 데이크스트라에, 단언과 줄어드는 양이라는 첫 싹은 튜링에 있습니다. sp와 wlp의 짝은 갈루아 연결의 전형적인 예이며, 수반 함자의 ∃와 ∀를 프로그램에 옮긴 것입니다. 반복문의 뜻과 wp를 최소 고정점으로 계산하는 방법은 영역 이론과 이어지고, 모든 프로그램을 자동으로 검증할 수 없는 이유는 정지 문제입니다. 조건들은 '그리고, 또는, 아니다'로 계산하는 불 대수⁠(Boolean algebra)⁠의 원소⁠(element)⁠이고, 전조건은 약하게 후조건은 강하게라는 결과 규칙은 하위 타입⁠(subtype)⁠의 반변⁠(contravariant)⁠·공변⁠(covariant)⁠과 같은 모양입니다. 메모리를 자원처럼 나눠 쓰는 분리 논리는 선형 논리와 닮았고, 명세를 타입⁠(type)⁠에 적어 증명과 프로그램을 한 몸으로 만드는 다른 길은 의존 타입⁠(dependent type)⁠과 증명 보조기⁠(proof assistant)⁠에 있습니다.