연역적 검증의 개요를 상기하고, IMP 언어에 대한 약한/강한 호어 논리 규칙을 제시한다. 이어서 다양한 반복문, goto와 조기 종료를 다루는 확장, 코루틴과 협력형 스레드를 위한 호어 논리를 소개하며, 예제 검증과 추가 읽을거리를 제공한다.
제14장 제어 구조를 위한 호어 논리
수학적 논리가 수학적 정의의 성질을 증명하기 위한 추론 원리를 제공하듯이, 프로그램 논리는 기능적 정확성과 같은 프로그램의 성질을 증명하기 위한 추론 원리를 제공한다. 이러한 논리 기반의 프로그램 검증 접근을 연역적 검증(deductive verification)이라 한다.
연역적 검증을 사용하려면 먼저 프로그램의 상태에 대한 논리적 단언(logical assertion)으로 프로그램에 주석을 단다. 예를 들면 다음과 같다.
그 다음, 프로그램 언어를 위한 프로그램 논리와 자동/대화형 정리 증명 도구의 도움으로, 사전조건이 불변식과 사후조건을 함축함을 증명할 수 있다.
예를 들어, 다음은 ACSL 명세 언어로 작성된 논리적 단언으로 주석이 달린 C 함수이다:
/@ requires \valid(a + (0..n-1)); assigns a[0..n-1]; ensures \forall integer i; 0 <= i < n ==> a[i] == 0; /void set_to_zero(int a, size_t n) { for (size_t i = 0; i < n; i++) { /@ invariant \forall integer j; 0 <= j < i ==> a[j] == 0 */ a[i] = 0; } }
requires(사전조건)은 set_to_zero에 전달되는 매개변수 a가 크기가 최소 n인 유효한 배열을 가리켜야 함을 말한다. ensures(사후조건)은 set_to_zero가 반환할 때 배열 a의 0부터 n−1까지의 원소가 0을 담고 있음을 말한다. assigns 절은 a의 이 원소들만 수정되고 그 밖의 메모리 위치는 수정되지 않음을 말한다. 마지막으로 루프의 invariant(불변식) 절은 배열 a의 처음 i개 원소가 이미 0으로 설정되었음을 단언한다.
튜링에서 플로이드, 그리고 호어까지. 연역적 검증은 처음에는 논리적 단언으로 주석이 달린 플로차트(제어 흐름 그래프, CFG)로 표현된 비구조적 프로그램의 맥락에서 개발되었다. 이 접근은 Turing (1949)의 초기 커뮤니케이션에서 처음 나타났으나, 정식 출판과 주석을 단 Morris and Jones (1984)에 이르기 전까지는 주목받지 못했다. 같은 접근이 독립적으로 Floyd (1967)에 의해 재발견되어 철저히 연구되었다.
그러나 프로그램 논리의 개념은 Turing (1949)과 Floyd (1967) 모두에서 부재하다. 대신, 이들은 프로그램 논리 다음 단계인, 주석이 달린 프로그램으로부터 검증 조건을 생성하는 데 초점을 둔다.
프로그램 논리를 연역적 검증의 기초로 제시한 것은 Hoare (1969)의 유명한 논문 “An Axiomatic Basis for Computer Programming”이다. 호어는 플로차트 대신 Algol 스타일의 구조적 프로그램을 고려한다. 이는 프로그램 논리와 구조적 제어가 깊이 얽혀 있기 때문에 중요하다. 프로그램 검증은 프로그램의 구조를 따를 뿐만 아니라, 프로그램 논리의 규칙은 프로그래밍 언어의 제어 구조와 거의 일대일로 대응한다. 이는 이 장의 나머지 부분에서 보여 준다.
호어 트리플. 대부분의 프로그램 논리와 마찬가지로, 호어 논리는 명령 c와 프로그램 변수 값에 대한 두 개의 논리적 단언(사전조건 P와 사후조건 Q) 사이의 3항 관계를 정의한다. 이러한 관계를 “호어 트리플(Hoare triple)”이라 하며 보통 [ P ] c [ Q ] 또는 { P } c { Q } 로 쓴다.
“강한 호어 트리플” [ P ] c [ Q ] 는, 명령 c가 사전조건 P를 만족하는 상태에서 시작되면 항상 오류 없이 종료하며, 최종 상태가 사후조건 Q를 만족함을 뜻한다.
“약한 호어 트리플” { P } c { Q } 는 유사하지만 종료를 보장하지는 않는다. 즉, 명령 c가 사전조건 P를 만족하는 상태에서 시작되면 오류 없이 실행되며, 만약 종료한다면 최종 상태가 사후조건 Q를 만족함을 뜻한다.
{ P } skip { P } (skip)
{ Q [x := e] } x := e { Q } (assign)
{ P } s 1 { Q } { Q } s 2 { R } (seq)
{ P } s 1; s 2 { R }
{ P ∧ b } s 1 { Q } { P ∧ ¬ b } s 2 { Q } (cond)
{ P } if b then s 1 else s 2 { Q }
{ P ∧ b } s { P } (while)
{ P } while b do s { P ∧ ¬ b }
P ⇒ P′ { P′ } s { Q′ } Q′ ⇒ Q (consequence)
{ P } s { Q }
그림 14.1: IMP 언어를 위한 약한 호어 논리의 규칙.
약한 호어 논리. 그림 14.1은 종료를 보장하지 않는 약한 호어 논리의 규칙을 보인다. 이 논리는 그림 6.1의 IMP 언어에 적용된다.
skip과 대입문에 해당하는 두 개의 공리가 있다. skip은 어떤 변수의 값도 바꾸지 않는다. 따라서, skip “이전”에 성립하던 프로그램 변수들에 대한 임의의 성질 P는 “이후”에도 성립한다. 즉, 모든 P에 대해 { P } skip { P } 다.
대입 x := e와 사후조건 Q를 생각하자. 사후조건 Q는 x의 모든 가능한 값에 대해 성립할 필요는 없고, 방금 x에 대입된 값 e에 대해서만 성립하면 된다. 따라서 Q [x := e] 가 대입 “이전”에 성립해야 한다. 이것이 (assign) 공리 { Q{x := e} } x := e { Q } 를 설명한다. 예를 들어,
{ 1 ≤ x + 1 < 10 } x := x + 1 { 1 ≤ x < 10 }
(consequence) 규칙은 명령 s의 사전조건과 사후조건을 조정할 수 있게 해 준다. 더 강하거나 동치인 사전조건 P로 P′를 대체할 수 있고(P ⇒ P′), 더 약하거나 동치인 사후조건 Q로 Q′를 대체할 수 있다(Q′ ⇒ Q). 예를 들어, (consequence)와 (assign) 규칙을 결합하면 다음을 얻는다.
0 ≤ x < 9 ⟹ 1 ≤ x + 1 < 10 { 1 ≤ x + 1 < 10 } x := x + 1 { 1 ≤ x < 10 } 1 ≤ x < 10 ⟹ 1 ≤ x < 11
{ 0 ≤ x < 9 } x := x + 1 { 1 ≤ x < 11 }
또한 이 두 규칙을 결합하여 플로이드의 대입 규칙도 보일 수 있다:
{ P } x := e { ∃ x 0, x = e [x := x 0] ∧ P [x := x 0] }
남은 세 규칙은 IMP의 세 가지 제어 구조의 본질을 포착한다: 순차, 조건, while 루프.
{ P } s 1 { Q } { Q } s 2 { R } (seq)
{ P } s 1; s 2 { R }
단언 Q는 s 1;s 2 실행 중의 중간 상태를 기술한다. Q는 s 1의 사후조건이자 s 2의 사전조건으로 작용한다. s 1;s 2의 사전조건은 s 1의 사전조건과 같고, s 2의 사후조건은 s 1;s 2의 사후조건과 같다.
{ P ∧ b } s 1 { Q } { P ∧ ¬ b } s 2 { Q } (cond)
{ P } if b then s 1 else s 2 { Q }
조건문의 두 분기 s 1과 s 2는 모두 사후조건 Q를 보장해야 한다. “then” 분기 s 1은 조건 b가 참임을 사전조건 P에 더해 가정할 수 있다. b가 거짓이면 이 분기는 실행되지 않기 때문이다. 마찬가지로 “else” 분기 s 2는 b가 거짓임을 P에 더해 가정할 수 있다.
{ P ∧ b } s { P } (while)
{ P } while b do s { P ∧ ¬ b }
while 루프의 사전조건 P는 루프 불변식으로 사용된다. 루프 본문 s는 처음에 P가 성립하고 루프 조건 b가 참임을 가정할 수 있다. 그런 다음 s가 끝날 때 P가 다시 성립함을 보장해야 하며, 그래야 다음 반복이 진행될 수 있다. 루프가 종료되면 불변식 P가 성립하고 조건 b는 거짓이다. 따라서 루프의 사후조건은 P ∧ ¬ b 이다.
{ 0 ≤ a } ⇒ { a = b · 0 + a ∧ 0 ≤ a } r := a; { a = b · 0 + r ∧ 0 ≤ r } q := 0; { a = b · q + r ∧ 0 ≤ r } while r ≥ b do ( { a = b · q + r ∧ 0 ≤ r ∧ r ≥ b } ⇒ { a = b · (q + 1) + (r − b) ∧ 0 ≤ r − b } r := r − b; { a = b · (q + 1) + r ∧ 0 ≤ r } q := q + 1 { a = b · q + r ∧ 0 ≤ r } ) { a = b · q + r ∧ 0 ≤ r ∧ r < b } ⇒ { q = a / b ∧ r = a mod b }
그림 14.2: 유클리드 나눗셈 알고리즘의 연역적 검증. s 1; { Q } s 2 는 Q가 s 1의 사후조건이자 s 2의 사전조건임을 뜻한다. { P } ⇒ { P′ } 는 결과 규칙의 적용을 나타낸다.
그림 14.2는 다음 유클리드 나눗셈 알고리즘을 약한 호어 논리로 검증하는 단계를 보인다:
r := a; q := 0; while r ≥ b do (r := r − b; q := q + 1)
초기에 a ≥ 0을 가정하면, 이 검증은 실행이 끝났을 때 q = a / b 및 r = a mod b 임을 보인다. 부분적 정확성만 증명했음을 주의하라. 종료는 보장하지 않는다: b ≤ 0이면 프로그램은 루프에 빠진다.
강한 호어 논리. 그림 14.3은 종료까지 보장하는 강한 호어 트리플 [ P ] c [ Q ] 의 규칙을 보인다. 루프 규칙을 제외하면, 규칙들은 약한 트리플의 규칙들과 유사하다. 실제로 skip과 대입문은 항상 종료하며, 순차와 조건문은 종료성을 보존한다. 오직 루프만이 while true do s 같은 발산을 유발할 수 있다.
∀ α, [ P ∧ b ∧ e = α ] s [ P ∧ 0 ≤ e < α ] (while)
[ P ] while b do s [ P ∧ ¬ b ]
while 루프의 규칙은 각 반복에서 엄격히 감소하는 변량(variant) 식 e의 도움으로 종료를 보장한다. e는 음이 아닌 정수 식이어야 한다. 복잡한 루프에서는 종료를 보이기 위해 사전식(lexicographic)으로 정렬된 다중 변량이 필요할 수 있다.
e의 감소는 유령 변수(ghost variable) α를 사용해 표현된다. 유령 변수는 대입할 수 없는 수학적 변수로, 사전조건과 사후조건에서 동일한 값을 갖는다. 따라서 s의 사전조건에 e = α가 있고 사후조건에 e < α가 있다는 것은 s의 실행 동안 e가 엄격히 감소함을 의미한다.
예를 들어, 그림 14.2의 유클리드 나눗셈 프로그램을 Ediv라 하자. 다음 강한 트리플을 증명할 수 있다:
[ a ≥ 0 ∧ b > 0 ] Ediv [ q = a / b ∧ r = a mod b ]
루프 변량은 변수 r이며, b > 0인 한 각 반복마다 엄격히 감소한다.
[ P ] skip [ P ] (skip)
[ Q [x := e] ] x := e [ Q ] (assign)
[ P ] s 1 [ Q ] [ Q ] s 2 [ R ] (seq)
[ P ] s 1; s 2 [ R ]
[ P ∧ b ] s 1 [ Q ] [ P ∧ ¬ b ] s 2 [ Q ] (cond)
[ P ] if b then s 1 else s 2 [ Q ]
∀ α, [ P ∧ b ∧ e = α ] s [ P ∧ 0 ≤ e < α ] (while)
[ P ] while b do s [ P ∧ ¬ b ]
P ⇒ P′ [ P′ ] s [ Q′ ] Q′ ⇒ Q (consequence)
[ P ] s [ Q ]
그림 14.3: IMP 언어를 위한 강한 호어 논리의 규칙
다른 종류의 루프. while 루프 외의 다른 유형의 루프에 대한 검증 규칙도 줄 수 있다. 이러한 규칙은 호어 논리의 규칙과, 해당 루프들을 while 루프로 인코딩하는 방식으로부터 도출할 수 있다.
예를 들어, 각 반복의 끝에서 종료 검사를 하는 do…while 루프에 대한 규칙은 다음과 같다:
{ P } s { Q } Q ∧ b ⇒ P
{ P } do s while b { Q ∧ ¬ b }
이는 do s while b 가 s; while b do s 와 동등함에서 따른다.
마찬가지로, 루프 본문 중간에 종료 검사가 있는 Ada 스타일 루프에 대한 규칙도 도출할 수 있다:
{ P } s 1 { Q } { Q ∧ ¬ b } s 2 { P }
{ P } loop s 1; exit when b; s 2 end { Q ∧ b }
계수형 for 루프는 더욱 흥미롭다. 루프 본문이 항상 종료한다면 루프가 종료함이 보장되기 때문이다. 다음과 같이 정의하자.
for i = ℓ to h do s 를 i := ℓ; while i ≤ h do (s; i := i + 1) 과 동등하다고 두자.
이 계수형 루프에 대해 다음 강한 호어 트리플을 도출할 수 있다:
i 및 FV(h)는 s 안에서 대입되지 않음 [ P ∧ ℓ ≤ i ≤ h ] s [ P [i := i+1] ]
[ P [i := ℓ] ∧ ℓ ≤ h − 1 ] for i = ℓ to h do s [ P [i := h + 1] ]
사전조건 ℓ ≤ h − 1 은 종료 시 i = h + 1 을 보장하는 가장 약한 사전조건이다. s에 대한 구문적 제약은 루프 본문 s의 실행 동안 i나 h의 자유변수들이 수정되지 않음을 보장한다. 그렇지 않으면, for i = 0 to 0 do i := i − 1 또는 for i = 0 to h do h := h + 1 같은 경우처럼 종료가 위태로워질 수 있다.
구문적 제약을 두는 대신, s의 시작과 끝에서 i와 h가 같은 값을 갖는다는 증명 의무를 추가할 수 있다:
∀ α β, [ P ∧ ℓ ≤ i ≤ h ∧ h = α ∧ i = β ] s [ P [i := i+1] ∧ h = α ∧ i = β ]
프로그램 논리에서 “goto” 다루기. 호어는 자신의 기념비적 논문의 결론에서 다음과 같이 쓴다.
실제로 어려움을 주는 영역은 레이블과 점프, 포인터, 그리고 이름 매개변수이다. 이러한 기능을 사용하는 프로그램의 증명은 장황해질 가능성이 있으며, 이는 근본 공리의 복잡성에 반영되는 것이 놀랍지 않다. (Hoare, 1969)
분명한 “실제 어려움” 하나는 goto 점프가 호어 논리 규칙에서 고려되지 않은 제어 흐름을 만든다는 점이다. 예를 보자:
if b then L: s else goto L
명령 s는 (조건 규칙이 단언하듯) b = true인 경우에만 진입되는 것이 아니라, 다른 경우에는 레이블 L로 점프가 수행되므로 b = false인 경우에도 진입될 수 있다. 이 사실을 반영하려면, 프로그램 논리는 s가 정상 실행 흐름으로 진입하든 goto L을 통해 진입하든 상관없이 s의 사전조건이 성립함을 보장해야 한다.
Clint와 Hoare의 goto 규칙. Clint and Hoare (1972)는 Algol 스타일의 블록 스코프 레이블과 goto에 대해 다음 규칙을 제안한다:
{ R } goto L { false } ⊢ { P } s 1 { R } { R } goto L { false } ⊢ { R } s 2 { Q } (label)
{ P } begin s 1; L: s 2 end { Q }
표기 A ⊢ B(“A가 B를 함의한다”로 읽음)는 자연 연역에서의 가설적 판단에 해당한다: 호어 논리의 규칙들에 더해 A를 가정하면 B를 도출할 수 있다는 뜻이다.
위 규칙의 전제들은 s 1과 s 2가 추가 전제 { R } goto L { false } 하에서 검증됨을 말하며, (consequence) 규칙을 사용해 { R } goto L { X } (임의의 단언 X)를 도출할 수 있다. 이는 s 2가 s 1 종료 후 정상적으로 진입하든, s 1이나 s 2 내부의 goto L을 통해 진입하든, s 2의 사전조건 R이 성립함을 보장한다.
goto L 문에 대한 공리는 없다. 점프에 대해 도출할 수 있는 트리플은 (scoped-label) 규칙이 도입한 가설적 판단 { R } goto L { false } 에서 따르는 것뿐이다.
Clint–Hoare 규칙의 쟁점. O’Donnell (1982)는 Clint and Hoare (1972)가 제안한 접근법의 미묘한 지점을 지적한다. 첫째, 동일한 이름의 레이블 L을 정의하는 중첩 블록의 경우
begin … begin … L: … end … L: … end
L에 연관된 “그” 사전조건이 모호해진다:
{ R 1 } goto L { false } ⊢ ( { R 2 } goto L { false } ⊢ X )
이 문제는 레이블 이름의 신선성(freshness)을 보장하도록 레이블들 중 하나의 이름을 바꾸어 해결할 수 있다.
둘째, { R } goto L { false } ⊢ A 의 논리적 처리에는 주의가 필요하다. 이는 논리적 함의 “{ R } goto L { false } 가 어떤 모형에서 A를 함의한다”로 다룰 것이 아니라, 논리적 함축(논리적 entailment)으로 다루어야 한다. 전자의 경우, { R } goto L { false } 는 호어 논리의 공리와 규칙들에 의해 제약되지 않으므로 거짓으로 둘 수 있다. 그러면 함의는 자명하게 성립하고, 다음과 같은 잘못된 호어 트리플을 도출할 수 있다:
{ false } goto L { false } ⟹ { true } goto L { false } { false } goto L { false } ⟹ { false } skip { false }
✘ { true } begin goto L; L: skip end { false }
첫 번째 전제는 함의 { false } goto L { false } ⟹ { true } goto L { false } 로 이해하면 참으로 간주될 수 있지만, 논리적 함축 { false } goto L { false } ⊢ { true } goto L { false } 로 이해하면 성립하지 않는다. (consequence) 규칙은 거짓 사전조건을 참 사전조건으로 바꾸는 것을 허용하지 않으며, 여기에는 적용 가능한 다른 규칙도 없기 때문이다.
Arbib–Alagic–de Bruijn 접근. goto 문을 보는 또 다른 방법은, 명령을 끝까지 실행하여 종료하는 것 외에 대안적인 종료 방식으로 간주하는 것이다. 명령에서 나가는 방식이 여러 개라면, 검증에서 각 종료 방식마다 하나씩 여러 개의 사후조건을 사용할 수 있다.
이 접근은 Arbib and Alagic (1979)이 처음 제안했고 de Bruin (1981)이 추가로 연구했다. 호어 트리플은 다음과 같은 4항으로 바뀐다.
{ P } s { Q } { J }
여기서 J(“jumps”의 J)는 레이블에서 단언으로의 사상(mapping)이다. 이 4항은 “명령 s가 사전조건 P를 만족하는 초기 상태에서 시작하여 정상적으로 종료한다면 최종 상태가 Q를 만족한다. 그리고 goto L 문을 수행하여 조기에 종료한다면, 그 시점의 상태는 J(L)을 만족한다”는 뜻이다. J 사후조건은 보통의 사후조건 Q처럼 약화시킬 수 있다.
P ⇒ P′ { P′ } s { Q′ } { J′ } Q′ ⇒ Q ∀L, J′(L) ⇒ J(L)
{ P } s { Q } { J }
항상 정상 종료하는 명령에 대해서는 J 사후조건을 false로 둘 수 있다:
{ P } skip { P } { λ L . false }
{ Q [x := e] } x := e { Q } { λ L . false }
J는 순차의 하위 명령들 사이에서 공유된다(조건문과 루프도 유사):
{ P } s 1 { R } { J } { R } s 2 { Q } { J }
{ P } s 1; s 2 { Q } { J }
goto L 문은 J(L)만 P이고 그 외 모든 사후조건은 false가 되게 할 수 있다. 여기서 J(L)는 goto의 사전조건 P이다:
{ P } goto L { false } { λ L′ . if L′ = L then P else false }
블록이 레이블 L을 명령 s 2에 연관시키는 경우, goto L로 나가는 모든 종료는 s 2의 사전조건 R을 만족해야 한다:
J′ = λ L′ . if L′ = L then R else J(L) { P } s 1 { R } { J′ } { R } s 2 { Q } { J′ }
{ P } begin s 1; L: s 2 end { Q } { J }
루프의 조기 종료. 여러 사후조건을 사용하는 요령은 break 문처럼 루프의 구조적 조기 종료에도 적용된다. 이 경우, 4항 { P } s { Q } { B } 를 사용할 수 있는데, 여기서 Q는 정상 사후조건이고 B는 break에 의한 조기 종료에 대한 사후조건이다. 다소 혼란스럽게도, B는 break 문의 사전조건이기도 하다:
{ B } break { false } { B }
break 문은 정상 종료하지 않으므로 정상 사후조건은 false로 둘 수 있다. while 루프에 대한 규칙은 다음과 같다:
{ P ∧ b } s { P } { Q } P ∧ ¬ b ⇒ Q
{ P } while b do s { Q } { false }
루프는 루프 본문 s에 의해 수행된 break 문을 잡아 정상적인 루프 종료로 바꾼다. 따라서 루프의 break 사후조건은 false가 될 수 있으며, 루프 본문의 break 사후조건은 루프의 정상 사후조건 Q가 된다.
파이썬 스타일의 else 절을 가진 while 루프(루프가 정상 종료할 때만 실행되고 break 시에는 실행되지 않음)에 대해 위 규칙을 확장할 수 있다:
{ P ∧ b } s { P } { Q } { P ∧ ¬ b } s′ { Q } { B }
{ P } while b do s else s′ { Q } { B }
조기 종료의 통합적 처리. 새로운 종료 방식을 추가할 때마다 사후조건을 하나씩 추가하는 대신, 함수 형태의 단일 사후조건을 사용할 수 있다:
Q : exit type ↦ assertion
종료 타입 K의 예는 다음과 같다.
K ::= norm 정상 종료 ∣ break(n) ∣ continue(n) 다단계 루프 종료 ∣ return(v) 함수 반환 ∣ goto(L) 점프 ∣ exn(E) 예외 발생
종료를 유발하는 명령들의 규칙은 모두 같은 모양을 갖는다:
{ P } skip { [norm ↦ P] } { P } break { [break(1) ↦ P] } { P } break n { [break(n) ↦ P] } { P } continue n { [continue(n) ↦ P] } { P } goto L { [goto(L) ↦ P] } { P } raise E { [exn(E) ↦ P] }
여기서 [K ↦ P] 는 함수 λ K′ . if K′ = K then P else false 를 뜻한다.
각 제어 구조는 하나 이상의 종료 타입을 처리하며, 해당 사후조건에 대한 제약을 추가한다. 예컨대 순차는 정상 종료를 처리한다:
{ P } s 1 { Q + [norm ↦ R] } { R } s 2 { Q }
{ P } s 1; s 2 { Q }
여기서 Q + [K ↦ P] 는 함수 λ K′ . if K′ = K then P else Q(K′) 를 뜻한다.
루프는 정상 종료에 더해 break와 continue 종료도 처리한다:
Q′ = Q + ⎡ ⎢ ⎢ ⎢ ⎢ ⎢ ⎣ norm ↦ P; break(1) ↦ Q(norm); break(n+1) ↦ Q(break(n)) continue(1) ↦ P; continue(n+1) ↦ Q(continue(n)) ⎤ ⎥ ⎥ ⎥ ⎥ ⎥ ⎦ { P ∧ b } s { Q′ } P ∧ ¬ b ⇒ Q(norm)
{ P } while b do s { Q }
레이블 L의 선언은 goto(L) 종료를 처리한다:
{ P } s 1 { Q + [norm ↦ R, goto(L) ↦ R] } { R } s 2 { Q + [goto(L) ↦ R] }
{ P } begin s 1; L: s 2 end { Q }
예외 처리자는 exn(E) 종료를 처리한다:
{ P } s 1 { Q + [exn(E) ↦ R] } { R } s 2 { Q }
{ P } try s 1 catch E → s 2 { Q }
IMP에 코루틴 추가. Clint (1973)은 다음과 같은 비대칭 코루틴 표현을 고려한다:
coroutine p = s 1 in s 2
소비자 s 2가 call p 를 수행하면, 생산자 s 1의 실행이 시작되거나, s 1이 가장 최근에 수행한 yield p 바로 다음부터 재개된다. 생산자 s 1이 yield p 를 수행하면, 소비자 s 2의 실행이 가장 최근에 수행한 call p 바로 다음부터 재개된다. 둘 중 하나(s 1 또는 s 2)가 종료하는 즉시 coroutine 명령은 종료한다. s 1과 s 2 사이의 값 교환은 공유 변수로 이루어진다.
var obs: int, c: int = 0, h: array [0..M] of int = { 0, ... } coroutine p = begin while c < N do h[obs] := h[obs] + 1; c := c + 1; yield p done end in ... obs = 12; call p; ... ... obs = 41; call p; ...
위 예에서, 코루틴 p는 관측값 obs의 히스토그램 h를 유지하며, N개의 값이 관측되면 멈춘다. 이 코루틴의 클라이언트는 다양한 obs 값(여기서는 12와 41)으로 p를 호출한다.
Clint의 코루틴 규칙. 각 코루틴 p에 대해 두 개의 단언 A p 와 B p 를 연관시킨다:
Clint (1973)은 코루틴 구성에 대해 다음 규칙을 제안한다:
{ B p } yield p { A p } ⊢ { A p } s 1 { Q } { A p } call p { B p } ⊢ { P } s 2 { Q }
{ P } coroutine p = s 1 in s 2 { Q }
점프에 대한 Clint–Hoare 규칙(14.3절)처럼, Clint의 코루틴 규칙도 전제에서 함축 ⊢ 를 사용한다. 생산자 s 1의 검증은 { B p } yield p { A p } 를 가정할 수 있고, 소비자 s 2의 검증은 { A p } call p { B p } 를 가정할 수 있다.
s 1과 s 2는 모두 coroutine 문의 사후조건 Q를 보장해야 한다. coroutine 문은 s 1 또는 s 2 중 하나가 종료하는 즉시 종료하기 때문이다.
생산자 s 1의 사전조건은 A p 이다. s 1은 s 2가 처음으로 p를 호출할 때 시작되며, 그 상태는 p의 사전조건 A p 를 만족한다. 반면 소비자 s 2의 사전조건은 전체 coroutine 문의 사전조건 P이다. s 2는 즉시 실행을 시작하기 때문이다.
아래는 위 “히스토그램” 예제의 검증 개요이다:
coroutine p = begin { I ∧ 0 ≤ obs ≤ M } while c < N do h[obs] := h[obs] + 1; c := c + 1; { I } yield p { I ∧ 0 ≤ obs ≤ M } done end in ... obs = 12; { I ∧ 0 ≤ obs ≤ M } call p; { I } ... ... obs = 45; { I ∧ 0 ≤ obs ≤ M } call p; { I } ...
불변식 I는 관측 수 c가 N을 넘지 않으며, 히스토그램의 합이 c와 같음을 나타낸다:
I ≜ c ≤ N ∧ c = ∑_{i=0}^{M−1} h[i]
각 call 문의 사전조건 A p 는 I ∧ 0 ≤ obs ≤ M 이다. 이는 h[obs] 접근이 경계를 벗어나지 않음을 보장한다. 사후조건 B p 는 c와 h를 연관짓는 정확성 불변식 I 그 자체이다.
IMP에 협력형 스레드 추가. 다음 명령을 생각하자:
run s 1 ∥ ⋯ ∥ s n end
명령 s 1, …, s n 의 실행은 서로 인터리브(interleave)된다. 각 명령은 자신을 중지하고 다른 명령으로 제어를 넘길 준비가 되면 yield 문을 수행한다. 두 개의 yield 문 사이에서는 실행이 순차적이다. run … end 명령은 모든 s i 가 종료하면 종료한다.
다음은 이러한 스타일로 작성된 생산자–소비자 모델의 예이다:
run (while true do while full do yield; data := produce(); full := true || while true do while not full do yield; consume(data); full := false) end
두 스레드는 data 공유 변수와 full 불리언 공유 변수로 이루어진 메일박스를 통해 값을 통신한다. full 변수는 data 변수가 유효한 값을 담고 있는지 여부를 나타낸다. 처음에는 full 이 false이다. 생산자 스레드(왼쪽)는 메일박스가 비어 있을 때(즉, full 이 false일 때)까지 기다린 다음 data에 값을 쓰고 메일박스를 비어 있지 않음으로 표시한다. 소비자 스레드(오른쪽)는 메일박스가 비어 있지 않기를 기다린다. 그런 다음 그 내용(data)을 꺼내 처리하고 메일박스를 비어 있음으로 표시한다.
협력형 스레드를 위한 규칙. run … end 구성에 대한 다음 검증 규칙은 코루틴에 대한 Clint 규칙의 대칭화된 버전이다:
{ P } yield { P } ⊢ { P } s i { Q } (i = 1,…,n)
{ P } run s 1 ∥ ⋯ ∥ s n end { Q }
사전조건 P는 각 “컨텍스트 전환” 시점—어떤 s i 가 yield 문으로 인해 실행을 시작하거나, 중단된 yield 가 재개될 때—에 성립하는 불변식이다. P는 yield의 사전조건이자 사후조건으로 작용한다. 실행은 어떤 s i 로든 시작할 수 있으므로, 모두 사전조건으로 P를 갖는다. 실행은 마지막으로 실행 중인 명령이 종료하면 종료한다. 그 명령은 s i 중 어떤 것일 수도 있으므로, 모든 s i 가 사후조건 Q를 보장해야 한다.
아래는 위 생산자–소비자 예제의 검증 개요이다. 교환되는 값 x에 대한 성질 R(x)를 생각하자(예: R(x) = 0 ≤ x < 10). produce와 consume 함수가 각각 이 성질을 보장/요구한다고 가정한다:
{ true } x := produce() { R(x) } { R(x) } consume(x) { true }
두 코루틴의 불변식 P는 메일박스가 비어 있지 않다면 그 내용이 R을 만족한다는 것이다:
P ≜ full = true ⟹ R(data)
다음과 같은 중간 단언을 사용하여 생산자와 소비자를 독립적으로 검증할 수 있다:
while true do { P } while full do { P } yield { P } ; data := produce(); { R(data) } full := true { P } || while true do { P } while not full do { P } yield { P } ; { full = true ∧ P } ⇒ { R(data) } consume(data); full := false { P }
생산자의 검증에서, produce가 반환한 값을 data에 설정하고 full 을 true로 만든 뒤에는 불변식 P가 다시 확립되므로, 반복을 계속할 수 있다.
소비자의 검증에서, while not full do 루프가 종료할 때 full 이 true이고 불변식 P가 성립함을 안다. 따라서 R(data)가 성립한다. 그러므로 data를 consume에 안전하게 전달할 수 있다. full 을 false로 설정한 뒤에는 불변식 P가 공허하게 성립하므로, 반복을 계속할 수 있다.
Winskel (1993) 9장과 10장은 호어의 공리적 스타일로 호어 논리를 자세히 다룬다. Nielson and Nielson (2007) 6장과 7장은 IMP의 작동 의미론(operational semantics)에 기초한 호어 논리의 대안적 제시를 제공한다.
15장(장 15)에서 설명하듯, 분리 논리(separation logic, Reynolds, 2002)는 힙 할당 데이터 같은 자원에 대해 추론하는 능력을 호어 논리에 확장한다. 동시 분리 논리(concurrent separation logic, O’Hearn, 2007)는 여기에 공유 메모리 동시성 지원을 추가한다. 두 논리는 호어 논리보다 더 강한 성질들을 증명할 수 있다. 예컨대 14.4절의 생산자/소비자 예제에서는 produce 함수가 할당한 모든 자원이 consume 함수에 의해 처분(dispose)됨을 증명할 수 있으며, 이는 통신 프로토콜에 의해 생성된 데이터가 유실되지 않음을 보여 준다.
프로시저와 함수는 Hoare (1969)가 언급한 “실제로 어려움을 주는 영역” 중 하나이다. 매개변수가 없고 비재귀적인 프로시저는 쉽게 다루어지지만, 재귀와 다양한 매개변수 전달 의미(값에 의한 전달, 참조에 의한 전달, 이름에 의한 전달)는 도전적이다. Apt (1981)은 이슈들과 프로시저/함수에 대한 제안된 호어 논리 규칙들을 개관한다. Parkinson et al. (2006)은 분리 논리를 사용해 이 이슈들을 재설명하고 호어 논리 규칙들을 재도출한다.
