어느 규칙을 골라도 답이 맞으려면, 무엇을 먼저 확인해야 할까요?

가드(guard, 실행을 허용하는 조건)는 해당 명령을 지금 실행해도 되는지 판정하는 참·거짓 조건입니다. ‘x≥y → m:=x’에서 x≥y가 가드이고 m:=x가 그 조건 아래 실행할 명령입니다. 가드가 참이면 실행 후보가 됩니다.

참인 가드가 둘 이상이면 그 가운데 어느 명령이 선택되어도 허용합니다. 위에 적힌 명령이 반드시 먼저 실행된다는 순서는 부여하지 않습니다. 어느 가드를 고를 확률이 얼마인지도 이 문법만으로 정해지지 않습니다.

원전은 대안 명령 묶음을 if와 fi로 둘러쌉니다. 이 글에서는 읽기 편하게 규칙 A·B라는 이름을 함께 붙이겠습니다. 실제 프로그래밍 언어의 if–else 우선순위와 혼동하지 않고, 원전이 정한 선택 규칙을 먼저 약속하는 것입니다.

x=y=5라고 대입해 보겠습니다. 첫 규칙의 가드 5≥5는 참이며 m에 x의 값 5를 저장합니다. 둘째 규칙의 가드 5≥5도 참이며 m에 y의 값 5를 저장합니다. 어느 경우에도 우리가 요구한 최댓값 조건을 만족합니다.

검증의 질문은 허용된 모든 경로가 원하는 결과 조건에 도달하는지입니다. 최댓값 예에서는 두 경로가 같은 최종 값을 만들므로 차이가 특히 작습니다. 다른 명령에서는 서로 다른 최종 값이 목표를 함께 만족할 수도 있습니다.

예를 들어 목표가 ‘m≥5’이고 가능한 명령들이 m:=5와 m:=6이라면 두 결과 모두 목표를 만족합니다. 반대로 목표를 ‘m=5’로 바꾸면 두 번째 결과는 맞지 않습니다. 같은 선택 묶음도 무엇을 보장하려는지에 따라 검증 결과가 달라집니다.

규칙을 ‘x>y → m:=x’와 ‘y>x → m:=y’로 바꾸어 보겠습니다. x와 y가 서로 다를 때는 여전히 큰 값을 고릅니다. 그러나 x=y=5라면 5>5가 양쪽에서 모두 거짓이므로 실행할 규칙이 없습니다.

원전의 대안 구성 if … fi는 모든 가드가 거짓인 상태에서 정상적으로 목표에 도달하는 명령으로 취급하지 않습니다. 이 글의 실험은 그 상태를 ‘실행 가능한 규칙 없음’으로 표시하고 결과 m을 성공 값처럼 만들지 않습니다.

입력에서 같은 값이 올 수 있다면 ≥를 >로 바꾸는 수정은 빠뜨린 경우를 만듭니다. 입력 조건을 x≠y로 제한하겠다고 명시하면 그 제한 안에서는 사용할 수 있습니다. 조건을 엄격하게 바꾸었다는 느낌과 입력 전체를 처리한다는 보장은 서로 다른 문제입니다.

새 규칙 A는 x≥0이면 y:=x+1, 규칙 B는 x≥2이면 y:=x−1이라고 정합시다. 목표는 y≥3입니다. x=2를 넣으면 두 가드가 모두 참입니다. A를 고르면 y=3이므로 목표에 도달합니다.

같은 시작 값에서 B를 고르면 y=1입니다. 이 선택도 문법이 허용하는 실행인데 목표를 만족하지 않습니다. 따라서 x=2에서 ‘목표를 얻는 길이 있다’는 말은 참이지만 ‘모든 허용된 선택이 목표를 보장한다’는 말은 거짓입니다.

이 글의 검증은 두 번째 요구를 사용합니다. 실험은 실행 가능한 분기들을 모두 계산하고 각 결과를 나란히 표시합니다. 하나의 성공을 찾아 다른 허용된 실패를 숨기지 않도록, 선택 목록과 목표 검사를 함께 읽어 보겠습니다.

명령을 실행하면 y 자리에는 x+1이 들어갑니다. 따라서 목표 y≥3에서 y를 x+1로 바꾸면 x+1≥3이라는 시작 조건을 얻습니다. 정수 x에서는 x≥2와 같은 조건입니다.

이 조건이면 실행 뒤 목표를 만족하고, x=1처럼 조건을 벗어나면 결과 y=2로 목표를 만족하지 못합니다. 필요 없이 더 좁은 조건을 붙일 수도 있습니다. x≥10으로 시작하면 목표를 얻지만 x=2부터 9까지의 가능한 입력을 괜히 제외합니다.

이렇게 원하는 종료 결과를 보장하는 가장 약한 시작 조건을 약한 전제조건(weakest precondition)이라고 부릅니다. 약하다는 말은 허술하다는 뜻으로 쓰지 않습니다. 목표를 보장하면서 허용할 수 있는 시작 상태를 모두 포함한다는 뜻입니다.

규칙 A의 결과 조건은 x+1≥3, 즉 x≥2입니다. 다만 A가 실행 후보인 x≥0인 경우에 그 결과 조건을 요구합니다. 규칙 B는 후보 조건 x≥2가 참일 때 x−1≥3, 즉 x≥4를 만족해야 합니다.

실행할 규칙이 하나 이상 있어야 한다는 조건도 필요합니다. 이 예에서는 x≥0 또는 x≥2, 곧 x≥0입니다. 이 조건에 두 분기의 안전 조건을 함께 붙이면, 0과 1에서는 A가 실패하고 2와 3에서는 B가 실패하며 4 이상에서는 두 규칙이 모두 성공합니다.

따라서 전체 대안 구성의 약한 전제조건은 x≥4입니다. 어느 분기를 실제로 고를지는 정하지 않았습니다. 그 선택의 자유를 그대로 남기고도 끝난 뒤 y≥3을 보장할 수 있는 시작 범위를 계산한 것입니다.

가드들을 B₁, B₂라고 하고 그 뒤의 명령을 S₁, S₂라고 부르겠습니다. 목표는 Q입니다. 먼저 B₁∨B₂는 실행할 수 있는 분기가 하나 이상 있다는 뜻입니다. 그다음 B₁⇒wp(S₁,Q)는 첫 가드가 참이면 첫 명령이 목표를 보장해야 한다는 뜻입니다.

둘째 분기에도 B₂⇒wp(S₂,Q)를 요구합니다. 세 조건을 모두 묶으면 (B₁∨B₂) ∧ (B₁⇒wp(S₁,Q)) ∧ (B₂⇒wp(S₂,Q))입니다. 여기에 들어간 ⇒는 이번에는 논리식의 조건문입니다. 가드와 명령을 잇는 → 표기와 역할을 구별해 읽습니다.

가드가 거짓인 분기의 결과를 무조건 목표에 맞출 필요는 없습니다. 그 분기는 지금 실행되지 않기 때문입니다. 반대로 가드가 참인 분기는 모두 검토해야 합니다. 이 두 점이 식 속 조건문에 담겨 있습니다.

원전은 반복 구성을 do와 od로 둘러쌉니다. 참인 가드가 있는 동안 그 가운데 하나의 명령을 실행하고, 새 상태에서 다시 가드들을 검사합니다. 모든 가드가 거짓이면 반복을 정상 종료합니다.

앞서 if … fi에서는 모든 가드가 거짓일 때 실행할 분기가 없다는 문제가 생겼습니다. do … od에서는 바로 그 상태가 반복을 마치는 조건입니다. 같은 가드 목록이라도 어떤 구성 안에 놓였는지에 따라 의미가 달라집니다.

따라서 반복이 끝났다는 정보를 얻으면 모든 가드의 부정을 함께 사용할 수 있습니다. 다만 종료할 때 참일 다른 성질도 필요할 수 있습니다. 다음 최대공약수 예에서, 반복 내내 유지되는 성질과 모든 가드가 거짓이라는 종료 조건을 결합해 보겠습니다.

양의 정수 x=12, y=8에서 시작하겠습니다. 규칙 A는 x>y이면 x:=x−y, 규칙 B는 y>x이면 y:=y−x입니다. x가 더 크므로 A를 실행하면 (x,y)=(4,8)이 됩니다. 이제 y가 더 커서 B를 실행하면 (4,4)가 됩니다.

두 수가 같아지면 x>y도 y>x도 거짓입니다. 따라서 반복이 정상 종료합니다. 마지막 같은 수 4가 처음 12와 8의 최대공약수라는 것을 주장하려면, 이 과정에서 최대공약수가 바뀌지 않았다는 이유를 보여 주어야 합니다.

입력 조건도 함께 지킵니다. 이번 반복의 대상은 양의 정수입니다. 0을 허용하면 큰 수에서 0을 빼는 동작이 값을 줄이지 않는 상황이 생깁니다. 실험은 양의 정수 범위를 명시하고 범위를 벗어난 입력에는 계산 결과를 만들어 주지 않습니다.

어떤 양의 정수 d가 x와 y를 모두 나눈다고 합시다. x=d·u, y=d·v로 쓸 수 있으므로 x−y=d·(u−v)입니다. 따라서 d는 x−y도 나눕니다. x와 y의 공약수는 x−y와 y의 공약수로 남습니다.

거꾸로 d가 x−y와 y를 모두 나누면, 두 수를 더한 (x−y)+y=x도 나눕니다. 그러므로 두 쌍의 공약수 집합은 같습니다. 그 집합에서 가장 큰 수인 최대공약수도 같습니다. y에서 x를 빼는 분기도 같은 방식으로 설명할 수 있습니다.

따라서 반복 동안 gcd(x,y)=gcd(처음 x, 처음 y)가 유지됩니다. 이런 성질을 반복 불변식(loop invariant, 반복 과정에서 계속 유지되는 조건)이라고 부릅니다. 마지막에 x=y라는 종료 조건을 더하면 gcd(x,y)=x=y이므로 반환할 값의 의미가 정해집니다.

그렇습니다. ‘끝난다면 결과가 맞다’와 ‘반드시 끝난다’는 서로 다른 요구입니다. 이번 반복에서는 양의 정수 x+y를 함께 살펴보겠습니다. x>y일 때 x를 x−y로 바꾸면 새 합은 x이고, 이전 합 x+y에서 양수 y만큼 줄어듭니다.

y>x인 분기에서는 새 합이 y가 되어 양수 x만큼 줄어듭니다. 두 수는 매 단계 양의 정수로 남습니다. 따라서 합은 양의 정수이면서 매 단계 엄격히 감소합니다. 이런 감소가 무한히 계속될 수 없으므로 어느 순간 더 실행할 가드가 없어져야 합니다.

종료를 보이는 감소량을 변량(variant, 반복할 때마다 줄어드는 값)이라고 부르겠습니다. 불변식은 바뀌지 않는 성질을 담당하고 변량은 끝없이 반복하지 않는 이유를 담당합니다. 이 둘과 종료 조건을 모아 처음의 최대공약수를 정확히 반환한다는 설명을 완성합니다.

x>0일 때 실행할 두 규칙을 새로 만들어 보겠습니다. 첫 규칙은 x를 그대로 두고, 둘째 규칙은 x에서 1을 뺍니다. 둘 다 가드가 x>0입니다. x=3에서 둘째 규칙을 계속 고르면 3,2,1,0을 거쳐 끝납니다.

그러나 첫 규칙을 계속 고르는 실행도 허용하면 x는 영원히 3에 머물 수 있습니다. 종료하는 길을 하나 찾았다는 사실만으로 모든 선택의 종료를 보장할 수는 없습니다. 가드 선택이 비결정적이라는 말에 공정한 선택이 자동으로 포함되는 것도 아닙니다.

앞의 최대공약수 반복은 어느 분기가 실행되어도 합이 줄었습니다. 그래서 특정 분기를 언젠가는 골라 줄 것이라는 별도 약속에 의존하지 않았습니다. 종료를 검증할 때는 허용한 모든 선택에서 감소 조건이 성립하는지를 확인해야 합니다.

지금 x와 y는 수학적 정수입니다. 실제 프로그램에서 정수 저장 범위가 정해져 있으면 덧셈이나 뺄셈이 범위를 넘는 경우의 실행 의미를 확인해야 합니다. 실험은 작은 양의 정수를 사용하며 수학적 계산과 같은 결과가 나는 범위로 제한했습니다.

입력 형식도 검증의 전제입니다. 최대공약수 실험은 소수나 음수를 양의 정수로 몰래 바꾸지 않습니다. 올바른 입력이 들어왔는지와 알고리즘이 그 입력에서 어떤 결과를 내는지는 나누어 다룹니다.

원전의 계산법은 명령과 목표의 관계를 체계적으로 정리하도록 도와줍니다. 그러나 임의의 요구를 넣으면 프로그램 전체를 자동으로 만들어 주는 알고리즘이라는 약속은 아닙니다. 어떤 불변식을 찾을지, 입력 범위를 어떻게 정할지는 여전히 문제의 성격을 이해하며 결정해야 합니다.

최댓값 실험에서는 같은 입력에서 열리는 모든 가드를 확인했습니다. ≥를 >로 바꾸었을 때 같은 값 입력이 빠진다는 사실도 찾았습니다. 이 과정은 ‘잘 작동한 예가 있다’에서 ‘어떤 입력을 처리하는가’로 질문을 넓힙니다.

두 번째 실험에서는 목표 y≥3에서 시작 조건 x≥4를 거꾸로 계산했습니다. x=2의 성공 경로와 실패 경로를 함께 보아야 그 조건을 얻을 수 있었습니다. 세 번째 실험에서는 최대공약수의 보존과 합의 감소를 나누어 살펴 결과의 의미와 종료를 함께 설명했습니다.

새 프로그램을 읽을 때도 입력 범위, 실행 가능한 선택, 끝에서 원하는 조건을 먼저 적어 보세요. 반복이 있으면 계속 유지할 성질과 줄어드는 값을 따로 찾을 수 있습니다. 검증의 질문을 구체적으로 정하면 어느 입력과 어느 선택을 더 조사해야 하는지도 드러납니다.