포인터·동적 메모리 및 다양한 자원을 다루는 분리 논리를 복습하고, 함수형-명령형 소언어(FUNREF)에 대한 분리 논리 규칙을 소개한다. 일반 callcc가 야기하는 비건전성을 보이는 예를 통해 전체 프로그램 스타일의 추론 규칙과 로컬 트리플 개념을 설명하고, 선형(원샷) 비한정 연속체와 효과 핸들러(선형 연속체)의 경우 표준 분리 논리로 모듈러하게 추론하는 방법(효과 프로토콜, 계속/중단 규칙, 핸들러 규칙)을 제시한다. 마지막으로 관련 연구를 간략히 정리한다.
분리 논리는 포인터와 동적 메모리 할당을 사용하는 프로그램을 더 잘 지원하기 위해 Hoare 논리를 확장한 것으로, Reynolds (2002)가 도입했다. 이러한 프로그램은 순수 Hoare 논리만으로 배제하기 어려운 문제들에 직면할 수 있다. 예를 들어, 별칭(aliasing: 서로 다른 포인터 변수가 동일 블록을 가리키는 경우)은 한 포인터 변수를 통해 쓰기가 다른 포인터 변수를 통한 읽기에 영향을 주도록 만들 수 있다. 더 이상 필요하지 않을 때 동적으로 할당된 블록의 해제를 잊어버리면 메모리 누수가 발생한다. 해제된 블록을 접근하면 미정의 동작을 초래한다. 이와 유사한 문제는 메모리 블록 이외에도 시스템 자원(파일 디스크립터 등), 보안 능력(capability), 그리고 이 장에서 나중에 보게 될 일부 유형의 연속체 등 많은 종류의 자원에서 발생한다.
Hoare 논리에서 어설션은 진리값을 가지며 프로그램의 가변 변수들의 현재 상태를 서술한다. 분리 논리에서는 어설션이 진리값과 함께 자원의 집합인 풋프린트(footprint)도 가지며, 이 자원들의 현재 상태와 이들이 어설션에 의해 유일하게 소유됨을 함께 서술한다. 이를 통해 분리 합성(separating conjunction) A ∗ B 같은 자원 인지적 논리 연결자를 정의할 수 있다. 이는 A와 B 두 어설션이 모두 성립하고 그 풋프린트가 서로 소 disjoint일 때 성립한다는 뜻이다. 따라서 A가 소유한 자원이 수정되어도, B가 소유한 자원은 수정되지 않았으므로 B는 계속 유효하게 남는다.
자원이 동적 할당 메모리 블록인 경우, 분리 논리의 어설션은 메모리 힙에 대한 술어가 된다. 아래는 흔히 쓰이는 어설션과, 힙 h에 대한 술어로서의 형식적 정의이다. D h는 h의 도메인, 즉 h에서 유효한 위치들의 집합을 뜻한다.
ℓ ↦ _ 위치 ℓ이 유효함 D h = {ℓ} ℓ ↦ v 위치 ℓ에 v가 들어 있음 D h = {ℓ} ∧ h(ℓ) = v emp 힙이 비어 있음 D h = ∅ ⟨ P ⟩ 논리 명제 P가 성립하고 힙은 비어 있음 D h = ∅ ∧ P A ∗ B 분리 합성 ∃ h 1, h 2, D h 1 ∩ D h 2 = ∅ ∧ h = h 1 ∪ h 2 ∧ A(h 1) ∧ B(h 2) A —∗ B 분리 함의(“magic wand”) ∀ h′, D h ∩ D h′ = ∅ ∧ A(h′) ⇒ B(h ∪ h′)
∃ n 1 n 2, ℓ 1 ↦ n 1 ∗ ℓ 2 ↦ n 2 ∗ ⟨ n 1 + n 2 = 10 ⟩
이는 ℓ 1 과 ℓ 2 가 어떤 정수 n 1, n 2 를 담고 있으며 그 합이 10인 유효 위치임을 말한다. 분리 합성을 사용하므로 ℓ 1 ≠ ℓ 2, 즉 포인터 ℓ 1 과 ℓ 2 사이에 별칭이 없음을 또한 보장한다. 결과적으로 ℓ 1 의 내용을 증가시키면, 다음을 안전하게 결론지을 수 있다.
∃ n 1 n 2, ℓ 1 ↦ n 1 ∗ ℓ 2 ↦ n 2 ∗ ⟨ n 1 + n 2 = 11 ⟩
이 결론은 ℓ 1 ≠ ℓ 2 보장이 없으면 성립하지 않는다. 두 포인터가 별칭이라면 ℓ 1 의 내용을 증가시키는 것은 ℓ 2 의 내용도 증가시켜 합이 12가 되기 때문이다.
The FUNREF language.그림15.1은 이 장에서 사용할 장난감 언어 FUNREF의 추상 구문을 보여준다. FUNREF는 ML 계열 언어(예: OCaml)처럼 제자리 변형 가능한 참조를 통해 명령형 프로그래밍을 지원하는 함수형 언어다. 참조는 다음 네 연산으로 제시된다:
할당은 비초기화이며 할당 해제는 명시적이라는 점에 유의하라. 이는 ML류나 Java류 언어와 달리 C류 언어와 유사하다.
Values: v::=c 상수 ∣ℓ 메모리 위치 ∣x 변수 ∣λ x . e 함수 추상 ∣v 1 op v 2 산술 연산 Computations: e::=v 자명한 계산 ∣let x = e 1 in e 2 계산의 순차 실행 ∣v 1 v 2 함수 적용 ∣if v then e 1 else e 2 조건문 ∣alloc 참조 할당 ∣! v 역참조 ∣v 1 := v 2 대입 ∣free v 할당 해제
Derived forms:
λ _ . e= λ x . e (단, x는 e에서 자유 변수가 아님) e 1; e 2=let x = e 1 in e 2 (단, x는 e 2에서 자유 변수가 아님) ref v=let x = alloc in x := v; x
그림 15.1: 표현식과 가변 참조로 이루어진 FUNREF 언어.
계산 람다-미적분(section11.2)에서 영감을 받아, FUNREF는 구문적으로 부수효과가 없는 순수한 표현인 값(values)과 참조를 생성·갱신·해제할 수 있는 효과적 표현인 계산(computations)을 구분한다. let x = e 1 in e 2 바인딩은 두 계산 e 1 과 e 2 의 실행을 순차화한다. 또한 e 2 가 e 1 의 값을 사용하지 않을 때 e 1; e 2 라고도 쓴다.
다음은 FUNREF 함수의 몇 가지 예시이다:
incr= λ r . let x = ! r in r := x + 1 swap= λ r 1 . λ r 2 . let x 1 = ! r 1 in let x 2 = ! r 2 in r 1 := x 2; r 2 := x 1 tally= λ r 1 . λ r 2 . let x 2 = ! r 2 in r 2 := 0; let x 1 = ! r 1 in r 1 := x 1 + x 2
함수 tally는 인자의 별칭에 민감한 함수의 예다. r 1 ≠ r 2 이면 r 2 의 내용을 r 1 에 더하고 r 2 를 0으로 설정한다. 그러나 r 1 = r 2 이면 r 1 과 r 2 모두 0이 된다.
A separation logic.그림15.2는 FUNREF를 위한 분리 논리의 규칙을 보여준다. Hoare 논리와 마찬가지로, 이 규칙들은 { P } e { Q } 삼중을 정의한다. 여기서 e는 계산이고, P는 그 사전 조건, Q는 사후 조건이다. 사전 조건 P는 e 실행 전의 상태를 서술하는 어설션이다. 사후 조건 Q는 e의 값을 어설션으로 사상하여 그 값이 반환될 때의 상태를 서술한다. P와 Q의 이러한 비대칭성 덕에, 효과뿐 아니라 계산의 값까지 명세할 수 있다. 예를 들면 다음과 같이 쓸 수 있다.
{ ⟨ x> 0 ⟩ } x−1 { λ v . ⟨ v = x−1 ∧ v ≥ 0 ⟩ }
P ⇒ Q v(pure)
{ P } v { Q }
{ P } e 1 { R } ∀v, { R v } e 2 [x := v] { Q }(let)
{ P } let x=e 1 in e 2 { Q }
{ P } e [x := v] { Q }(fun)
{ P } (λ x . e)v { Q }
{ P ∗ ⟨ v = true ⟩ } e 1 { Q } { P ∗ ⟨ v = false ⟩ } e 2 { Q }(cond)
{ P } if v then e 1 else e 2 { Q }
{ emp } alloc { λ ℓ . ℓ ↦ _ }(alloc)
{ ℓ ↦ v } ! ℓ { λ r . ⟨ r = v ⟩ ∗ ℓ ↦ v }(deref)
{ ℓ ↦ _ } ℓ := v { λ _ . ℓ ↦ v }(assign)
{ ℓ ↦ _ } free ℓ { λ _ . emp }(free)
{ P } e { Q }(frame) { P ∗ R } e { λ v . Q v ∗ R }
P ⇒ P′ { P′ } e { Q′ } ∀v,Q′v ⇒ Q v(consequence)
{ P } e { Q }
그림 15.2: FUNREF 언어를 위한 분리 논리 규칙.
규칙 (pure)와 (let)은 자명한 계산과 계산의 순차 실행을 서술한다:
P ⇒ Q v(pure)
{ P } v { Q }
{ P } e 1 { R } ∀v, { R v } e 2 [x := v] { Q }(let)
{ P } let x=e 1 in e 2 { Q }
이 두 규칙은 Hoare 논리의 (skip) 규칙과 (assign) 규칙(그림14.1)에 상응한다. 특히 (let) 규칙으로부터, 순차식 e 1;e 2 에 대한 규칙을 유도할 수 있다.
{ P } e 1 { λ _. R } { R } e 2 { Q }(seq)
{ P } e 1; e 2 { Q }
규칙 (cond)와 (consequence)도 Hoare 논리의 그것과 유사하다. 반면 (frame) 규칙은 분리 논리의 특징적 규칙이다:
{ P } e { Q }(frame)
{ P ∗ R } e { λ v . Q v ∗ R }
이 규칙은 분리 논리의 핵심 성질을 활용한다. 만약 { P } e { Q } 가 성립한다면, 어설션 P와 Q v(e의 값 v에 대한)가 e에 중요한 모든 위치를 서술한다. P나 Q v의 풋프린트에 속하지 않는 어떤 위치도 e의 평가에 영향을 미치지 않으며, 이 평가 동안 수정되지 않는다. 따라서 사전 조건 P ∗ R이 성립하면, 초기 힙 중 R이 서술하는 부분은 e의 실행 동안 변하지 않으며, 실행이 끝났을 때도 R이 성립하고 사후 조건 Q v ∗ R이 참이 된다.
참조에 대한 네 연산은 이른바 “작은(small)” 규칙으로 주어진다.
{ emp }alloc { λ ℓ . ℓ ↦ _ } { ℓ ↦ v }! ℓ { λ r . ⟨ r = v ⟩ ∗ ℓ ↦ v } { ℓ ↦ _ }ℓ := v { λ _ . ℓ ↦ v } { ℓ ↦ _ }free ℓ { λ _ . emp }
여기서 작은 것은 규칙이 아니라 사전/사후 조건의 풋프린트다. 예컨대 대입 ℓ := v에 대한 규칙은 위치 하나 ℓ만을 담은 힙으로 서술되며, 대입 후에 v가 들어 있음을 보장한다. 더 큰 힙을 다루려면 “작은” 규칙과 프레임 규칙을 결합하여 다음과 같은 “큰” 규칙을 얻으면 된다.
{ P }alloc { λ ℓ . ℓ ↦ _ ∗ P } { ℓ ↦ v ∗ P }! ℓ { λ r . ⟨ r = v ⟩ ∗ ℓ ↦ v ∗ P } { ℓ ↦ _ ∗ P }ℓ := v { λ _ . ℓ ↦ v ∗ P } { ℓ ↦ _ ∗ P }free ℓ { λ _ . P }
이 규칙들과 그림15.2의 규칙들을 사용하면, 앞서 제시한 incr, swap, tally 함수에 대해 다음 명세들을 증명할 수 있다:
{ ℓ ↦ n }incr ℓ { λ _ . ℓ ↦ n+1 } { ℓ 1 ↦ n 1 ∗ ℓ 2 ↦ n 2 }swap ℓ 1 ℓ 2 { λ _ . ℓ 1 ↦ n 2 ∗ ℓ 2 ↦ n 1 } { ℓ 1 ↦ n 1 ∗ ℓ 2 ↦ n 2 }tally ℓ 1 ℓ 2 { λ _ . ℓ 1 ↦ n 1 + n 2 ∗ ℓ 2 ↦ 0 }
여러 제어 연산자들(예: callcc, 비제한 효과 핸들러)은 원래 한 번만 실행될 프로그램 조각을 여러 번 또는 전혀 실행하지 않게 할 수 있다. 이는 이러한 제어 연산자를 위한 프로그램 논리의 설계를 크게 복잡하게 만든다. 다음은 Timany and Birkedal (2019)에서 가져온 예다:
let x = ref 0 in let f = e in incr x; f(); ! x
여기서 e는 x를 언급하지 않으며 unit에서 unit으로 가는 함수를 반환하는 표현식이다. x가 0에서 시작하고 e에 의해 영향받지 않으며, 그 후 한 번 증가되고, f() 호출에도 영향받지 않고, 마지막에 반환되므로 위 예는 항상 1을 반환하리라 기대한다. 이제 e를 다음 표현으로 바꿔 보자:
e = callcc(λ k . λ _ . throw k(λ _ . ()))
callcc가 바인딩하는 연속체 k는 λ f . incr x; f(); … 이다. 이는 정확히 incr x 직전에서 시작해 프로그램 끝까지 확장된다. e가 완료되면 f는 λ _ . throw k(λ _ . ())에 바인딩되고, 그 다음 incr x가 한 번 실행된 뒤 f가 적용된다. 연속체 k가 재시작되어 f를 λ _ . ()로 바인딩하고 incr x를 두 번째로 실행한다. 마지막 ! x는 2를 반환한다.
다음은 가변 상태를 수반하지 않는 callcc의 또 다른 기묘한 예다:
let f = e in let n = f()in n × 0
여기서 e는 unit → int 형의 표현식이다. 이 예는 n × 0 = 0이 모든 정수 n에 대해 성립하므로 항상 0을 반환해야 한다. 이는 (let)과 (pure) 규칙으로 증명할 수 있다:
{ P } f() { Q } ∀n,Q n ⇒ ⟨ n × 0 = 0 ⟩ ∗ Q n(pure) { Q n } n × 0 { λ r . ⟨ r=0 ⟩ ∗ Q n }(let)
{ P } let n = f()in n × 0 { λ r . ⟨ r=0 ⟩ ∗ Q n }
그러나 e = callcc(λ k . λ _ . throw k 1)인 경우, f() 호출은 let n = f()in n × 0이 n × 0의 계산을 건너뛰고 1을 반환하게 만든다.
이러한 예들이 보여주듯, 완전하고 비제한적인 callcc와 비제한 (let), (frame) 규칙의 조합은 비건전하다.
Timany and Birkedal (2019)는 (let) 규칙을 callcc나 throw를 포함하지 않는 표현으로 제한하고, callcc와 throw에 대해서는 전체 프로그램, 작동적(operational) 스타일의 규칙을 사용해 추론하는 방식으로 이 문제를 회피할 것을 제안한다. 보다 정확히, 그들은 먼저 임의의 부분식 e가 아닌 전체 프로그램 p에 적용되는 규칙 {{ P }} p {{ Q }} 를 정의한다. 각 규칙은 p를 C[e 1]로 분해하는 데 적용되며, 여기서 C는 평가기 문맥이고 e 1은 축약 가능한 부분식이다. 예를 들어, let, 조건문, callcc, throw에 대한 규칙은 다음과 같다:
P ⇒ Q v
{{ P }} v {{ Q }}
{{ P }} C[e [x := v]] {{ Q }}
{{ P }} C[let x=v in e] {{ Q }}
{{ P }} C[e 1] {{ Q }} {{ P }} C[if true then e 1 else e 2] {{ Q }}
{{ P }} C[e 2] {{ Q }} {{ P }} C[if false then e 1 else e 2] {{ Q }}
{{ P }} C[v(cont C)] {{ Q }} {{ P }} C[callcc v] {{ Q }}
{{ P }} C′[v] {{ Q }}
{{ P }} C[throw(cont C′)v] {{ Q }}
이 추론 규칙들과 section8.4의 callcc 축약 규칙 사이의 유사성에 주목하라. 각 축약 규칙 p → p′마다, “{{ P }} p {{ Q }} 를 증명하려면 {{ P }} p′ {{ Q }} 를 증명하면 충분하다”라고 말하는 대응되는 추론 규칙이 있다. 이는 일종의 기호적 실행을 수행하여 프로그램 실행에 대해 추론할 수 있게 해준다. 예를 들어, 다음 장난감 프로그램이 n+2로 계산됨을 보일 수 있다:
{ emp } n + 2 { λ x.⟨ x=n+2 ⟩ }(**) { emp } (throw(cont([ ] + 2))n + 4) + 2 { λ x.⟨ x=n+2 ⟩ }(*)
{ emp } callcc(λ k.throw k n + 4) + 2 { λ x.⟨ x=n+2 ⟩ }
여기서 (*)는 문맥 C = [ ] + 2 에 대해 callcc 규칙을, (**)는 문맥 C = ([ ] + 4) + 2 에 대해 throw 규칙을 사용한다.
검증을 용이하게 하고 분리 논리의 모듈러 추론 능력을 어느 정도 회복하기 위해, Timany and Birkedal (2019)는 로컬 트리플 { P } e { Q } 를, 임의의 문맥 C에서 사용할 수 있는 삼중으로 정의한다. 보다 정확히, 로컬 트리플은 다음 문맥 규칙을 만족하는 삼중이다.
{ P } e { Q } ∀v, {{ Q v }} C[v] {{ R }}(context)
{{ P }} C[e] {{ R }}
일반 분리 논리 규칙(그림15.2에 나타난 규칙들)로 유도 가능한 모든 삼중이 로컬 트리플임을 보일 수 있다. 이를 통해 callcc나 throw를 사용하지 않는 프로그램 부분에 대해서는 표준 분리 논리와 (let), (frame) 규칙의 전체 위력을 이용하여 정상적으로 추론할 수 있다. 오직 callcc와 throw가 관련된 프로그램 부분만 전체 프로그램, 작동적 추론을 필요로 한다.
section15.3 서두에서 보았듯, callcc와 다른 제어 연산자들이 추론을 어렵게 만드는 이유 중 하나는 포획된 연속체가 여러 번 실행될 수 있다는 점이다. Timany and Birkedal (2019)의 예에서,
let x = ref 0 in let f = e in incr x;f(); ! x
표현식 e의 연속체는 두 번 실행된다. 한 번은 e가 정상적으로 반환할 때, 또 한 번은 f가 적용되어 e가 포획한 연속체가 호출될 때다.
이 장의 나머지에서 보듯, 정확히 한 번 사용되는 선형(linear) 또는 많아야 한 번 사용되는 어파인(affine) 연속체는 이러한 문제를 보이지 않으며 표준 분리 논리로 기술될 수 있다. 문헌에서 원샷(one-shot) 연속체라고 불리는 이러한 연속체는 예외 구현(section8.3), 협력형 멀티스레딩(sections8.3, 10.4), 이터레이터에서의 제어 역전(sections8.7, 10.3) 등 많은 제어 연산자 응용에 충분하다. 연속체가 여러 번 호출되는 유일한 경우는 백트래킹(섹션8.3, 8.7의 choose-and-assert 예)이나 비결정성(section12.2의 flip 효과)을 구현할 때다.
The call1cc operator는 Bruggeman et al. (1996)이 도입한 callcc의 “원샷” 변형이다. 사용 형태는 callcc와 같다:
call1cc(λ k . e)
현재 연속체를 포획하여 e의 평가 동안 k에 바인딩한다. 그러나 k는 정확히 한 번만 사용되어야 한다. e에서 정상적으로 반환하는 것도 k의 한 번 사용으로 간주된다. 따라서 e는 세 가지 가능한 동작을 가진다:
다음은 지역 예외처럼 연속체를 사용하는 동작 1과 2의 예시다:
λ n . call1cc(λ k . − (if n< 0 then n else throw k n)
n< 0 이면 call1cc의 본문이 n의 음수로 정상 반환한다(동작 1). n ≥ 0 이면 연속체 k가 n으로 적용되어 call1cc가 n을 반환한다(동작 2).
다음은 동작 3의 예시다. 이 예는 yield 함수를 호출하여 서로에게 제어를 넘김으로써 실행을 교차하는 두 개의 코루틴을 구현한다.
let coroutine f g = call1cc(λ k 0 . let ready = alloc in let yield = λ () . call1cc(λ k . let k′ = ! ready in ready := k;throw k′())in let terminate = λ x . let k′ = ! ready in discard k′;free ready;throw k 0 x in call1cc(λ k . ready := k;let x = f yield in terminate x); let x = g yield in terminate x)
두 코루틴은 인자 함수 f와 g이며, 둘 다 인자로 yield 함수를 받는다. 타입은 (unit → unit) → unit이다. 먼저 종료 연속체 k 0을 포획하고, 이어 원소 하나짜리 ready 큐를 할당한다. 이 큐는 현재 실행 중이지 않은 코루틴의 연속체를 담는 참조일 뿐이다. yield 함수는 자신의 연속체 k를 포획하고 ready에 담긴 연속체 k′와 교환한 다음 k′를 재시작한다. terminate 함수는 f나 g 중 하나가 종료될 때 호출된다. 종료 연속체 k 0을 호출하기 전에 ready에 있는 연속체를 명시적으로 폐기(discard)한다. 이는 각 연속체를 정확히 한 번만 사용한다는 정책에 부합한다. 마지막으로, ready는 g yield의 실행을 시작할 연속체로 초기화되고, f yield가 실행된다. f 또는 g가 반환하면 terminate가 호출되고 전체 coroutine 함수가 반환된다.
Specifying continuations. 1차 근사로, 연속체는 결코 반환하지 않는 함수로 볼 수 있다. 따라서 연속체는 사전 조건(값에서 어설션으로 가는 함수)만 가지며, 이는 연속체가 필요로 하는 자원을 서술하고 함수 인자의 값을 제약한다. 사후 조건은 없다. 우리는 iscont k P를 k가 사전 조건 P를 가진 연속체임을 뜻하는 표기로 쓴다. k를 포획한 call1cc의 사후 조건 또한 P임에 유의하라. 왜냐하면 k를 값 v에 적용하면 해당 call1cc가 v로 반환되기 때문이다.
선형 연속체와 함수 사이의 주요 차이는, 함수는 여러 번 호출되거나 전혀 호출되지 않을 수 있지만 선형 연속체는 정확히 한 번 사용되어야 한다는 점이다. 따라서 iscont k P는 순수 어설션이 아니다. 비어 있지 않은 풋프린트를 가지며 복제하거나 무시할 수 없다.
emp⇍ ⇏iscont k P⇍ ⇏iscont k P ∗ iscont k P
직관적 근거는 각 연속체가 자신의 스택에서 실행될 수 있다는 점이다. 이는 효과 핸들러의 OCaml 구현에서와 같다(섹션10.2 참조). 따라서 iscont k P는 이 스택을 담는 메모리 영역의 소유권을 주장(assert)한다.
연속체 명세에는 흥미로운 “프레이밍” 성질이 있다. P v ∗ R 자원을 요구하는 연속체 k를 생각해 보자. 이는 누락된 자원 R이 사용 가능하고 분리해 둘 수 있다면 더 적은 자원 P v만 요구하는 것으로 볼 수 있다:
iscont k(λ v . P v ∗ R) ∗ R ⟹ iscont k P
동치로, 이 성질은 iscont의 단조성 성질로도 쓸 수 있다:
(∀ v,P v —∗ P′v) ⟹ iscont k P′ —∗ iscont k P
Rules for linear continuations.iscont 어설션을 사용하여 call1cc, throw, discard 연산자에 대한 다음 분리 논리 규칙을 줄 수 있다.
{ iscont k P ∗ P v } throw k v { λ _ . false }
{ iscont k P } discard k { λ _ . emp }
{ P ∗ iscont k Q } e { λ v . Q v ∗ iscont k Q } { P } call1cc(λ k . e) { Q }
throw k v가 안전하게 실행되려면, k는 사전 조건 P를 가진 유효한 연속체여야 하며 P v가 만족되어야 한다. 따라서 사전 조건은 iscont k P ∗ P v이다. throw k v는 정상적으로는 반환하지 않으므로 사후 조건은 λ _ . false이며, 이는 결과 규칙(consequence)로 임의의 사후 조건 Q로 대체할 수 있다.
call1cc(λ k . e)의 경우, 본문 e는 사전 조건으로 P ∗ iscont k Q를 가정할 수 있다. 여기서 P는 call1cc 표현의 사전 조건이고 Q는 그 사후 조건이다. 실제로 k의 어떤 적용도 call1cc 표현의 반환점으로 점프하므로 사후 조건 Q를 보장해야 한다. e가 값 v로 정상 종료하면, Q v 사후 조건뿐 아니라 k를 전혀 사용하지 않았음을 증거하는 iscont k Q 어설션 또한 보장해야 한다.
An example of verification.이제 앞의 두 코루틴 예의 검증을 개략적으로 설명한다. section14.4의 코루틴과 협력 스레드에 대한 Hoare 논리 규칙에서 영감을 받아, “문맥 전환”(즉, f나 g가 yield 연산을 실행할 때)마다 어떤 불변식 P가 성립한다고 가정한다. P는 또한 f와 g의 사전 조건이어야 하고, 두 함수는 동일한 사후 조건 Q를 공유해야 함이 드러난다. 따라서 f와 g가 다음 계약을 만족한다고 가정한다:
∀ R, { P ∗ R } yield() { λ _ . P ∗ R }⊢ { P ∗ R } f yield { λ v . Q v ∗ R } ∀ R, { P ∗ R } yield() { λ _ . P ∗ R }⊢ { P ∗ R } g yield { λ v . Q v ∗ R }
전칭된 명제 R은 yield 구현의 내부 불변식이다. 이제 이를 사용해 코루틴 함수 내부의 ready 참조와 종료 연속체 k 0을 서술한다. 이를 위해 다음과 같이 둔다.
R = ∃ k,ready ↦ k ∗ iscont k(λ _ . P ∗ R) ∗ iscont k 0 Q
R은 재귀적임에 유의하라. ready에 저장된 연속체 k를 호출하기 전에는 사용자 불변식 P뿐 아니라, 적절한 연속체 k′를 ready에 저장함으로써 내부 불변식 R도 복원되어야 한다. 이는 yield가 정확히 하는 일이며, 다음 검증 개요에서 볼 수 있다:
let yield = λ () . { P ∗ R } call1cc(λ k . { P ∗ R ∗ iscont k(λ _ . P ∗ R) } let k′ = ! ready in { P ∗ ready ↦ k′ ∗ iscont k′(λ _ . P ∗ R) ∗ iscont k(λ _ . P ∗ R) ∗ iscont k 0 Q } ready := k; { P ∗ ready ↦ k ∗ iscont k′(λ _ . P ∗ R) ∗ iscont k(λ _ . P ∗ R) ∗ iscont k 0 Q } ⇒ { P ∗ R ∗ iscont k′(λ _ . P ∗ R) } throw k′()) { P ∗ R }
따라서
{ P ∗ R } yield() { λ _ . P ∗ R }
이 성립하며, 이는 f의 명세에 따라
{ P ∗ R } f yield { λ v . Q v ∗ R }
를 함의하고, g에 대해서도 마찬가지다. 또한 다음을 보일 수 있다.
{ Q v ∗ R } terminate v { λ _ . false }
yield와 terminate의 이러한 명세로부터 다음이 따른다.
{ P ∗ iscont k 0 Q ∗ ready ↦ _ } call1cc(λ k . { P ∗ iscont k 0 Q ∗ ready ↦ _ ∗ iscont k(λ _ . P ∗ R) } ready := k; { P ∗ R } let x = f yield()in { Q x ∗ R } terminate x); { P ∗ R } let x = g yield()in { Q x ∗ R } terminate x
이로써 함수 coroutine의 검증이 끝난다.
효과 핸들러(챕터10)는 여러 면에서 callcc와 다르다. 특히 핸들러는 한정(delimited) 연속체를 받는 반면 callcc는 비한정(undelimited) 연속체를 포획한다. 그러나 프로그램 논리로 효과 핸들러에 대해 추론할 때, 코드 조각이 반복 실행되는 문제는 동일하게 발생한다. 비결정성의 Flip 효과(section12.2)를 보자:
handle let b = perform Flip in incr x with val(x) → x Flip(_, k) → continue k false;continue k true
이 예에서 perform Flip은 두 번 반환한다. 한 번은 값 false로, 또 한 번은 값 true로. 이는 incr x가 두 번 실행되게 한다. 이는 표준 (let) 규칙이 고려하지 않는다.
그러나 핸들러가 포획하는 연속체를 선형, 즉 정확히 한 번만 사용되도록 제한할 수 있다. 이는 OCaml이 하는 방식이다(섹션10.2 참조). 이 경우, 분리 논리의 비제한 (let), (frame) 규칙을 사용해 효과 핸들러에 대해 추론할 수 있다. 이는 de Vilhena and Pottier (2021)의 Hazel 논리가 하는 바다.
Effect protocols. 모듈러 검증을 지원하기 위해, de Vilhena and Pottier (2021)는 효과를 수행하는 코드 조각과 효과를 처리하는 코드 조각 사이의 계약으로 작동하는 효과 프로토콜(effect protocol) 개념을 도입했다. 프로토콜 Ψ의 구문은 다음과 같다:
Ψ::=⊥ 효과 없음 ∣!x(F v) { P } .?y(w) { Q } 효과 F에 대한 프로토콜 ∣Ψ 1 + Ψ 2 두 프로토콜의 합집합
프로토콜 ⊥는 어떤 효과도 수행될 수 없음을 말한다. 프로토콜 Ψ 1 + Ψ 2 는 Ψ 1 또는 Ψ 2 가 허용하는 임의의 효과가 수행될 수 있음을 말한다. 프로토콜 !x(F v) { P } .?y(w) { Q } 는 모든 x의 선택에 대해, 사전 조건 P가 성립하면 인자 값 v로 효과 F를 수행할 수 있고, 이어 어떤 y의 선택에 대해 F의 결과 값 w가 사후 조건 Q를 만족할 것임을 말한다. 여기서 P와 Q는 분리 논리 어설션이며, x와 y는 v, P, Q에 등장할 수 있는 수학적 변수들의 집합이다.
예를 들어, 예외처럼 동작하는 Abort 효과에 대한 프로토콜은 다음과 같다. perform Abort는 결코 반환하지 않으며 Abort의 핸들러는 포획된 연속체를 폐기한다.
!(Abort()) { true } .?y(y) { false }
false 사후 조건은 이 효과가 결코 반환하지 않음을 나타낸다.
다음은 카운터 증가를 시뮬레이션하는 Next 효과에 대한 프로토콜이다:
!n(Next()) { Count n } .?(n) { Count(n+1) }
추상 어설션 Count n은 카운터의 현재 값을 추적한다. 만약 카운터가 단일 메모리 위치 ℓ로 구현된다면
Count n ≜ ℓ ↦ n
으로 둘 수 있다. 그러나 여러 메모리 위치를 포함하는 더 복잡한 구현도 가능하며 적절한 Count 술어 내부에 숨길 수 있다. 계약에 따르면, Next는 어떤 n 값에 대해 Count n이 성립하는 임의의 상태에서 수행 가능하며, perform Next는 Count(n+1)이 성립하는 상태에서 값 n을 반환한다.
Reset 효과를 추가하여 카운터를 0으로 설정하는 Next 프로토콜을 확장할 수 있다:
!n(Next()) { Count n } .?(n) { Count(n+1) } +!n(Reset()) { Count n } .?(()) { Count 0 }
Separation logic. 분리 논리는 네중 { P } e ⟨ Ψ ⟩ { Q } 를 정의한다. 여기서 e는 표현식이고, P는 그 사전 조건, Q는 e가 정상적으로 반환하는 경우를 서술하는 정상 사후 조건이며, Ψ는 e가 수행할 수 있는 효과를 서술하는 효과 프로토콜이다. 이는 점프(goto)용 Hoare 논리(section14.3)와 유사하다. Arbib-Alagic-de Bruijn 접근은 정상 사후 조건 Q와 s가 수행할 수 있는 점프를 지정하는 “goto 프로토콜” J를 함께 쓰는 네중 { P } s { Q } { J } 를 사용한다.
그림15.2의 분리 논리 규칙은 네중으로 곧장 확장된다. (pure)와 (let) 규칙에서처럼 Ψ 사후 조건은 무시되거나 부분 계산들에 분배된다:
P ⇒ Q v(pure)
{ P } v ⟨ Ψ ⟩ { Q }
{ P } e 1 ⟨ Ψ ⟩ { R } ∀v, { R v } e 2 [x := v] ⟨ Ψ ⟩ { Q }(let)
{ P } let x=e 1 in e 2 ⟨ Ψ ⟩ { Q }
(consequence) 규칙은 두 사후 조건 Ψ와 Q를 약화할 수 있게 해준다:
P ⇒ P′ { P′ } e ⟨ Ψ′ ⟩ { Q′ } ∀v,Q′v ⇒ Q v Ψ′ ⊑ Ψ(consequence)
{ P } e ⟨ Ψ ⟩ { Q }
관계 Ψ′ ⊑ Ψ는 Ψ가 Ψ′보다 더 허용적(permissive)임을 의미한다. 즉, Ψ′가 허용하는 모든 효과는 Ψ도 허용하고, 동일하거나 더 제한적인 프로토콜을 갖는다. (정의의 정확한 형태는 de Vilhena and Pottier (2021) 참조.)
Performing effects. perform 구성의 규칙은 다음과 같다:
P ⇒ Ψ allows (F v) { Q }(perform)
{ P } perform(F v) ⟨ Ψ ⟩ { Q }
여기서 Ψ allows (F v) { Q } 는 효과 F를 인자 v로 수행하고, 그 효과가 반환할 때 Q가 성립하도록 하는 데 필요한 조건을 뜻한다. 이 조건은 다음 등식들로 정의된다:
⊥ allows (F v) { Q }= false Ψ 1 + Ψ 2 allows (F v) { Q }= Ψ 1 allows (F v){Q} ∨ Ψ 2 allows (F v) { Q } !x(F v′) { A } .?y(w) { B } allows (F v) { Q } = ∃ x,⟨ v′ = v ⟩ ∗ A ∗ (∀ y,B —∗ Q(w))
마지막 경우는 다음과 같이 해석된다. 실제 인자 v와 계약의 형식 매개 v′가 같도록 x를 선택할 수 있다면, F의 사전 조건 A가 성립해야 하며, F의 사후 조건 B를 만족시키는 임의의 y 선택에 대해, 사후 조건 Q(w)가 성립해야 한다.
앞의 두 경우는 직관적이다. ⊥ 계약은 어떤 효과도 수행할 수 없게 하고, Ψ 1 + Ψ 2 계약은 Ψ 1 또는 Ψ 2 가 허용하는 효과를 수행할 수 있게 한다.
Specifying continuations. section15.4와 마찬가지로, 효과 핸들러가 포획한 연속체 k를 명세하기 위해 특수 어설션 iscont k P Ψ Q를 도입한다. 이 연속체들은 한정(delimited)되어 있으므로, 적용 가능한 값을 서술하는 사전 조건 P와, 반환 가능한 값들을 서술하는 Q, 수행 가능한 효과를 서술하는 Ψ라는 두 개의 사후 조건을 가진다. 이런 점에서 한정 연속체는 함수와 닮았다. 그러나 함수는 여러 번 적용될 수 있는 반면, 우리의 한정 연속체는 선형이며 정확히 한 번 적용되어야 한다. 따라서 iscont k P Ψ Q 술어는 복제 가능하지 않다. 더구나 P에 대해 단조적(monotone)이다:
(∀ v,P v —∗ P′v) ⟹ iscont k P′Ψ Q —∗ iscont k P Ψ Q
한정 연속체에 대한 두 연산은 continue(연속체 재시작)와 discontinue(연속체 폐기)이며, 그 규칙은 단순하다:
{ iscont k P Ψ Q ∗ P v }continue k v ⟨ Ψ ⟩ { Q } { iscont k P Ψ Q }discontinue k ⟨ ⊥ ⟩ { λ _ . emp }
Handling effects. section10.5와 동일한 표기를 사용한다: handle e with e ret, e eff 는 e가 수행하는 효과를 e eff로 처리하고 e의 반환 값을 e ret으로 처리한다. 얕은(shallow) 처리 의미론을 가정한다. 이 구성에 대한 분리 논리 규칙은 다음과 같다:
{ P } e ⟨ Ψ ⟩ { Q } ishandler ⟨ Ψ ⟩ { Q } (e ret, e eff) ⟨ Ψ′ ⟩ { Q′ }
{ P } handle e with e ret, e eff ⟨ Ψ′ ⟩ { Q′ }
핸들러가 e의 결과(반환 값과 효과)를 다른 결과로 변환하는 것을 서술하듯, ishandler 술어는 e의 사후 조건 ⟨ Ψ ⟩ { Q } 를 핸들러의 사후 조건 ⟨ Ψ′ ⟩ { Q′ } 로 어떻게 변환하는지를 서술한다.
만약 e가 정상 종료하면 그 값 v는 Q를 만족하고 e ret v가 실행된다. 따라서 이 계산은 다음을 만족해야 한다.
{ Q(v) } e ret v ⟨ Ψ′ ⟩ { Q′ }
만약 e가 인자 v와 연속체 k를 가진 효과 F를 수행하면서 종료하면, e eff(F v)k가 실행되며 다음을 만족해야 한다.
{ R } e eff(F v)k ⟨ Ψ′ ⟩ { Q′ }
여기서 어떤 사전 조건 R에 대해 성립해야 한다. R이 값 v, 연속체 k, e eff가 사용할 수 있는 자원에 대해 무엇을 보장할 수 있을까? Ψ에서 F에 연결된 프로토콜을 찾아, 수행된 효과 F v에 대한 사전 조건 A와 사후 조건 B를 도출할 수도 있다. 그러면 핸들러 e eff(F v)k 안에서 A가 성립한다고 가정할 수 있고, k가 사전 조건 B와 사후 조건 ⟨ Ψ ⟩ { Q } 를 가진 연속체라고 가정할 수 있다. (얕은 핸들러를 고려하므로, 연속체가 실행될 때는 핸들러가 적용되지 않으니 e의 사후 조건과 동일하다.)
R=A ∗ iscont k B Ψ Q
대안으로, 그리고 더 간결하게, de Vilhena and Pottier (2021)는 Ψ의 allows 술어 의미에서 F에 대해 허용된 임의의 인자 값과 임의의 연속체로서 v와 k를 특징짓는다. 이는 e eff(F v)k에 대한 다음 사전 조건으로 이어진다:
R= Ψ allows (F v) { λ x . iscont k(λ y . ⟨ y=x ⟩)Ψ Q }
이는 다음과 같이 읽을 수 있다. 프로토콜 Ψ가 F v에 대해 허용하는 임의의 응답 x에 대해, 연속체 k는 x에 적용될 수 있고 그 후 사후 조건 ⟨ Ψ ⟩ { Q } 를 만족한다.
모든 것을 합치면 다음과 같다.
ishandler ⟨ Ψ ⟩ { Q } (e ret, e eff) ⟨ Ψ′ ⟩ { Q′ } ≜⎛ ⎝∀ v, { Q(v) } e ret v ⟨ Ψ′ ⟩ { Q′ }⎞ ⎠ ∧⎛ ⎝∀ v,k,{ Ψ allows (F v) { λ x . iscont k(λ y . ⟨ y=x ⟩)Ψ Q } } e eff k v ⟨ Ψ′ ⟩ { Q′ }⎞ ⎠
이 ishandler 정의는 효과 처리의 얕은 의미론에 대응한다. 깊은(deep) 핸들러에 대응하는 정의는 de Vilhena and Pottier (2021)를 보라.
O’Hearn (2019)은 분리 논리와 그 응용에 대한 개요를 제공한다. 분리 논리는 포인터 프로그램과 선형 연속체에 대한 추론을 넘어 많은 용도를 가진다. 특히 동시성으로의 확장인 동시 분리 논리(concurrent separation logic, O’Hearn, 2007)는 비협력 멀티스레딩과 공유 메모리 병렬성에 대한 추론의 필수 도구이다.
효과 핸들러와 기타 제어 연산자에 대한 프로그램 논리는 활발한 연구 분야다. 우리는 단순하고 그에 해당하는 규칙이 (비한정 연속체에 대한) goto 점프와 (한정 연속체에 대한) 함수 적용 규칙과 유사하기 때문에 선형(원샷) 연속체의 경우를 강조했다. Delbianco and Nanevski (2013)는 일반(멀티샷) 연속체를 가진 callcc에 대한 Hoare 논리를 개발했다. de Vilhena (2022, chapter 6)의 Maze 분리 논리는 제한된 프레임 규칙의 대가로 일반(멀티샷) 연속체를 가진 효과 핸들러에 적용된다. 이는 효과를 통한 인코딩으로 callcc에 대한 추론을 지원한다. van Rooij and Krebbers (2025)는 어파인(원샷) 또는 일반(멀티샷) 연속체를 가진 효과 핸들러를, 어파인 효과를 추적하는 부분구조 타입 시스템을 사용해 통합적으로 다룬다.
이 장에서 언급한 제어 연산자에 대한 프로그램 논리들(Timany and Birkedal, 2019, de Vilhena and Pottier, 2021, de Vilhena, 2022, van Rooij and Krebbers, 2025)은 Iris 분리 논리 프레임워크(Jung et al., 2018)를 사용해 개발되었고 Rocq 증명 도우미로 기계 검증되었다.
