프로그램이 올바른 답을 낸다는 것을 어떻게 증명할까요?

이 글에서는 a를 0 이상의 정수, b를 1 이상의 정수로 정합니다. a=0도 괜찮습니다. 연필이 없으면 묶음 수와 나머지가 모두 0입니다. a<b이면 한 묶음도 만들지 않고 q=0, r=a로 끝납니다.

이렇게 실행 전에 갖추어야 하는 조건을 사전조건(precondition, 실행을 시작할 때의 약속)이라고 부릅니다. 이번 사전조건은 a≥0 ∧ b>0입니다. 기호 ∧는 양쪽 조건이 모두 성립한다는 뜻입니다. a와 b는 실행 내내 고정하며, q와 r만 바꿉니다.

또한 이 글의 증명에서는 정수 계산이 정확하고, 숫자가 커져도 넘침이 생기지 않는 수학적 모형을 씁니다. 실제 실험 화면은 작은 정수만 입력받습니다. 기계가 숫자를 저장하는 방식까지 다루려면 그 계산 규칙을 따로 확인해야 합니다.

P에는 사전조건을, C에는 실행할 명령을, Q에는 실행 뒤에 확인할 조건을 넣습니다. Q는 사후조건(postcondition, 실행을 마친 뒤의 약속)입니다. 예를 들어 {x=7} x:=x+3 {x=10}은 처음 x가 7이고 x에 3을 더해 저장하면, 실행이 끝났을 때 x가 10이라는 뜻입니다.

이 글의 세 부분 표기 {P} C {Q}는 오늘날 널리 쓰는 호어 트리플(Hoare triple, 사전조건·명령·사후조건의 세 묶음)입니다. 원논문은 같은 역할을 P {C} Q로 적습니다. 중괄호의 위치가 달라도 시작 조건, 명령, 끝 조건이라는 역할을 따라 읽으면 됩니다.

여기에는 중요한 단서가 있습니다. 호어의 기본 규칙은 실행이 성공적으로 끝났을 때 사후조건이 성립한다고 말합니다. 반복이 반드시 끝난다는 보장은 나중에 별도의 근거로 붙입니다. 이 구분을 부분정당성(partial correctness, 종료한 실행의 결과가 맞음)이라고 부릅니다.

:=는 대입 기호입니다. 오른쪽을 지금의 값으로 계산한 다음 그 결과를 왼쪽 변수에 저장하라는 명령입니다. 처음 x가 7이라면 오른쪽 x+3을 먼저 계산해 10을 얻고, 그 10을 x의 새 값으로 저장합니다.

앞의 x와 뒤의 x를 구분해 적으면 x_새값=x_옛값+3입니다. 실행 전에는 7, 실행 뒤에는 10을 가리킵니다. 대입 뒤에도 이전의 7을 기억해야 하는 증명에서는 별도의 고정된 이름을 사용합니다.

이 규칙은 오른쪽 식을 계산하는 동안 다른 변수가 저절로 바뀌지 않는다는 전제 아래 적용합니다. 호어도 논문에서 부수효과(side effect, 식을 계산하면서 다른 상태까지 바꾸는 작용)를 별도로 주의합니다. 이 글의 덧셈과 뺄셈에는 그런 부수효과가 없습니다.

실행 뒤에 원하는 조건은 x≥10입니다. 명령은 x:=x+3이므로, 실행 뒤의 x 자리에 실행 전의 x+3을 넣어 봅니다. 시작할 때 x+3≥10이어야 하고, 이를 정리하면 x≥7입니다.

그래서 {x≥7} x:=x+3 {x≥10}을 얻습니다. 처음 x가 7이면 10, 8이면 11입니다. 경계 바로 아래인 6에서는 9가 되어 목표를 충족하지 못합니다. 아래 실험은 시작값·더할 수·목표를 바꾸어 이 대입 역산을 실제로 계산합니다.

호어의 대입 공리는 이 과정을 일정한 형식으로 적습니다. 사후조건 Q에서 대입 대상 x의 자유로운 자리를 식 E로 바꾼 조건을 Q[x←E]라고 하면, {Q[x←E]} x:=E {Q}입니다. 지금처럼 변수가 단순하고 식의 계산에 부수효과가 없는 범위에서 사용합니다.

명령의 실행 순서를 따라 중간 조건을 둡니다. 첫 명령 r:=a가 끝나면 r=a입니다. 다음 명령 q:=0은 r이나 a를 건드리지 않으므로 이 관계가 유지되면서 q가 0이 됩니다. 따라서 두 명령 뒤에는 a=b×0+r이 성립합니다.

앞 명령의 결과가 뒤 명령을 시작할 조건을 마련해 주면, 둘을 하나로 이어 증명할 수 있습니다. 이를 합성 규칙(rule of composition, 명령들을 순서대로 이어 증명하는 규칙)이라고 합니다. 중간 조건이 앞뒤 명령의 증명을 연결합니다.

이번에는 a≥0도 이미 정했으므로 초기 r은 0 이상입니다. 초기화를 마친 상태에서 a=bq+r ∧ r≥0을 얻었습니다. 이제 반복할 때마다 이 관계를 되찾을 수 있는지 살펴보겠습니다.

한 묶음을 만들 때 q를 1 늘리고 r에서 b를 뺍니다. 완성한 묶음으로 옮겨 간 연필과 아직 남아 있는 연필을 더하면 처음 수 a입니다. 이 관계가 a=bq+r입니다. 17자루와 묶음 크기 5에서는 아래 표의 각 줄에서 오른쪽 계산이 모두 17이 됩니다.

반복의 시작점과 한 차례 실행을 마친 지점마다 유지하는 조건을 루프 불변식(loop invariant, 반복의 경계에서 유지되는 관계)이라고 부릅니다. 이 글에서는 I: a=bq+r ∧ r≥0을 사용합니다. q도 0에서 시작해 정수 1씩 증가하므로 계속 0 이상의 정수입니다.

불변식은 값이 변하지 않는다는 뜻과 다릅니다. q와 r은 변합니다. 둘이 이루는 관계가 반복의 경계에서 유지됩니다. 또한 반복문 안의 모든 줄에서 같은 식이 성립해야 하는 것은 아닙니다. 두 대입 사이에는 다음 질문의 중간 조건이 필요합니다.

정확히 그 중간에는 다른 조건을 써야 합니다. 처음 q=0, r=17에서 r:=r−5만 실행하면 q=0, r=12입니다. 이때 5q+r=12입니다. 이어 실행할 q 증가를 미리 반영한 17=5(q+1)+r이 중간 조건입니다.

일반적으로 반복 직전의 a=bq+r에서 r의 옛값을 r_옛값이라고 적겠습니다. 새 r은 r_옛값−b이므로 b(q+1)+(r_옛값−b)=bq+r_옛값=a입니다. 그 뒤 q를 q+1로 바꾸면 다시 a=bq+r이 됩니다.

순서대로 실행하는 두 줄을 한꺼번에 동시 대입한 것처럼 읽으면 이 중간 상태를 놓칩니다. 불변식의 위치를 반복 시작과 반복 끝으로 정하면, 중간 조건을 거쳐 같은 관계로 돌아오는 증명이 분명해집니다.

반복문은 뺄셈을 하기 전에 b≤r인지 검사합니다. 한 묶음 분량이 남아 있을 때만 r:=r−b를 실행하므로 새 r은 0 이상입니다. r=7, b=5이면 2를 얻고, 다음에는 5≤2가 거짓이어서 뺄셈을 멈춥니다.

불변식의 유지 증명에는 이렇게 두 전제를 함께 씁니다. 반복 시작점에서 I가 성립하고, 들어가기 직전에 검사한 조건 B가 참입니다. 여기서 B는 b≤r입니다. I∧B에서 반복 몸체를 실행한 뒤 I를 다시 얻으면 됩니다.

가드를 검사하지 않고 남은 2에서 다시 5를 빼면 −3이 됩니다. 그 명령은 우리가 증명한 반복문과 다릅니다. 반복문에 붙은 조건까지 함께 보아야 원래 증명의 적용 범위를 판단할 수 있습니다.

반복이 끝났다면 들어가는 조건 b≤r이 거짓입니다. 정수의 순서에서 이는 r<b를 뜻합니다. 불변식에 포함한 r≥0까지 합하면 0≤r<b가 됩니다.

불변식의 다른 부분 a=bq+r도 함께 남습니다. 두 사실을 모아 a=bq+r ∧ 0≤r<b라는 원래 목표를 얻습니다. 실제 값에서는 17=5×3+2이고 0≤2<5입니다.

반복 규칙의 구조는 {I∧B} 몸체 {I}에서 {I} while B do 몸체 {I∧¬B}를 얻는 것입니다. ¬B는 반복 조건이 거짓이라는 뜻입니다. 이 단계에서는 종료한 실행의 결과를 증명했으며, 종료 자체는 다음 질문에서 확인합니다.

반복 때마다 줄어드는 양을 따로 확인합니다. 이번에는 r이 그 역할을 합니다. 사전조건에서 b는 1 이상의 정수이므로, 한 차례 실행할 때 r은 적어도 1 줄어듭니다. 동시에 반복의 경계에서 r은 0 이상입니다.

0 이상의 정수가 매번 엄격하게 줄어드는 과정은 끝없이 이어질 수 없습니다. 이 프로그램은 r이 b보다 작아지면 멈추며, a=17,b=5에서는 17, 12, 7, 2의 순서로 내려갑니다. a=0이면 처음부터 조건이 거짓이므로 반복을 한 번도 하지 않고 끝납니다.

이렇게 감소량을 이용해 종료를 증명하는 설명은 원논문의 기본 부분정당성 규칙에 덧붙인 교육적 보강입니다. 호어는 §4에서 자신의 제시한 규칙만으로 성공적인 종료를 증명할 수 없다고 명시합니다. 결과가 맞는다는 증명과 종료 증명을 합쳐 이번 수학적 모형에서의 전체 정당성을 확인합니다.

a=17,b=0을 넣어 보겠습니다. 반복 조건 0≤r은 r=17일 때 참입니다. r에서 0을 빼므로 r은 계속 17입니다. q는 0, 1, 2처럼 늘지만 0q+17=17이라는 관계는 계속 유지됩니다.

불변식이 성립한다는 사실만으로 종료를 보장할 수 없다는 예입니다. b가 0이면 r이 엄격하게 감소한다는 근거가 사라집니다. 우리가 처음 정한 사전조건 b>0이 이 입력을 제외합니다.

실험 화면에서는 b=0을 허용해 이 경계 사례를 보여 주되, 무한 반복을 실제로 돌리지 않습니다. r이 변하지 않고 가드가 계속 참이라는 구조를 계산하여 설명합니다. 화면을 안전하게 멈추는 처리와 원래 프로그램이 종료한다는 주장은 구분합니다.

a=17,b=5,q=0,r=17에서 r을 12로 만든 뒤 q를 2로 바꾸면, 계산한 합계는 5×2+12=22입니다. 처음 수 17과 어긋납니다. 반복 몸체가 불변식을 보존해야 한다는 단계에서 이 오류가 드러납니다.

또 다른 오류도 있습니다. 반복 조건을 b<r로 바꾸면, a=15,b=5일 때 r이 5가 된 순간 멈춥니다. 결과는 q=2,r=5입니다. 합계 15=5×2+5는 맞지만 목표 r<5는 실패합니다. 마지막 한 묶음을 처리할 수 있는 등호가 빠졌기 때문입니다.

첫 오류는 불변식 유지에서, 둘째 오류는 종료 뒤 목표를 얻는 단계에서 드러납니다. 아래 비교 실험은 이 두 오류와 묶음 수를 전혀 올리지 않는 오류를 같은 입력으로 실행합니다. 결과를 보고 어떤 조건이 깨졌는지 확인할 수 있습니다.

프로그램을 실행하는 기계의 산술 규칙이 증명에서 사용한 규칙과 맞는지 확인해야 합니다. 이 글은 정수 덧셈과 뺄셈을 정확하게 수행하는 수학적 모형을 택했습니다. 실제 구현에는 저장 가능한 최대값이나 계산 중 넘침 처리가 있을 수 있습니다.

예를 들어 0, 1, 2, 3만 표현하는 가상의 장치에서 3+1을 계산한다고 합시다. 넘침을 오류로 처리하면 결과가 없고, 최대값에 붙들어 두면 3, 나머지 연산으로 순환시키면 0입니다. 같은 기호 +를 썼어도 결과가 달라집니다. 호어는 논문 §2에서 이러한 선택을 공리와 함께 다룹니다.

따라서 무한 정수에 대한 증명을 그대로 유한 장치에 옮길 때는, 실행 중 모든 값이 허용 범위 안에 머무는지 확인하거나 해당 장치의 산술 규칙으로 다시 증명해야 합니다. 이번 웹 실험은 a를 0~100, b를 0~20의 작은 정수로 제한하므로 계산값이 자바스크립트의 정확한 정수 범위 안에 있습니다.

먼저 입력의 범위를 a≥0,b>0인 정수로 정하고 a와 b를 고정합니다. 초기화 뒤에 I:a=bq+r ∧ r≥0이 성립함을 확인합니다. 이어 I∧b≤r에서 반복 몸체를 실행하면, 중간 조건을 거쳐 I가 다시 성립함을 대입과 계산으로 보였습니다. 이 계산은 특정한 17과 5에 기대지 않습니다.

반복이 끝나면 r<b이고 I가 남으므로 목표 a=bq+r ∧ 0≤r<b를 얻습니다. 여기에 b가 양의 정수여서 r이 매번 엄격히 감소한다는 종료 근거를 더합니다. 그러면 이 수학적 모형의 모든 허용 입력에 대해 몫과 나머지를 구한다는 결론이 나옵니다.

호어의 논문이 제시한 것은 명령과 조건을 연결하는 작은 규칙들의 체계입니다. 이 글의 세 실험은 그 체계를 따라 직접 값을 계산하고 오류를 관찰하는 학습 도구입니다. 임의의 프로그램을 입력받아 증명하는 도구는 구현하지 않았습니다. 40편의 분리 논리는 여기서 더 나아가, 메모리의 일부를 바꾸는 동안 다른 부분의 관계를 어떻게 보존할지 다룹니다.