규칙 하나가 생성자 하나🔗

§1.3의 Proof와 같은 모양이다. 전제가 인자이고 결론이 결과 타입이다. Lean의 화살표가 Reynolds의 가로선 노릇을 한다.

규칙 몇 개에 눈여겨볼 점이 있다.

대입

사후조건에서 사전조건을 만든다. 방향이 거꾸로다. 아래에서 따로 본다.

순차 합성

가운데 단언 r이 전제에만 나온다. 규칙이 r을 정해 주지 않으므로 유도하는 사람이 골라야 한다. §3.4의 주석 명세가 이 선택을 적는 방법이다.

반복

i가 불변식이다. 규칙은 불변식을 찾아 주지 않는다. 프로그램 검증에서 사람이 하는 일의 대부분이 이 선택이다.

결과 규칙

전제 Stronger p' p는 ∀ σ, ⟦p'⟧ σ → ⟦p⟧ σ다. 단언 사이의 함의가 타당하다는 의미적 사실이고, 1장의 Proof로 증명했다는 뜻이 아니다. Hoare 논리는 단언 논리를 오라클로 쓴다. 완전성을 말할 때 "단언의 타당성에 상대적으로"라는 단서가 붙는 이유다(책은 완전성을 §3.8 참고문헌에서 7장의 wp로 미루고 본문에서 다루지 않는다; 보충 Wlp.lean에서 미리 본다).

SP와 WC는 각각 생성자이고, conseq는 두 규칙을 이어 만든 제공 정리다. 다음 여섯 연습은 서로의 풀이에 의존하지 않는다.

CA의 전체 판에서는 두 전제가 내놓은 종료 상태가 같은 명령의 결과임을 쓴다. DA는 사전조건의 선언을 나눈다. CSP와 CST는 Comm.eval_agree_outside_fa와 coincidence_assert로 쓰이지 않는 변수의 단언을 옮긴다. CST의 종료 상태는 전제가 준다.

첫 유도는 대입 공리 하나와 결과 규칙 하나다.

유도 규칙 — ISK · MSQₙ · RASₙ🔗

SK와 SP만으로도 한 줄짜리 파생 규칙이 나온다.

MSQₙ(§3.3 pp.60–61)은 순차 합성 n개를 결과 규칙으로 잇는 가족이다. MSQ₁은 p₀ ⇒ q₀, {q₀} c₀ {p₁}, p₁ ⇒ q₁에서 {p₀} c₀ {q₁}를 내는데, 이미 있는 Hoare.conseq와 글자 그대로 같다. 책은 MSQₙ을 MSQₙ₋₁에 SQ와 결과 규칙 한 겹을 더 둘러 유도한다(가정 있는 증명의 예) — 그 한 겹을 n = 2에서 직접 보인다.

힌트: MSQ₁(Hoare.conseq h₀ hc₀ h₁)로 왼쪽 명령을 {p₀} c₀ {q₁}까지 올리고, WC (Hoare.weaken hc₁ h₂)로 오른쪽을 {q₁} c₁ {q₂}까지 내린 뒤 SQ로 잇는다. 일반 n은 같은 겹을 반복할 뿐이다.

RASₙ(§3.3 pp.61–62)은 대입만 늘어선 명령 v₀ := e₀ ; ⋯ ; vₙ₋₁ := eₙ₋₁의 전제를 반복 치환 하나로 압축한다. 대입 목록은 머리 (v, e)와 꼬리로 나눠 rasComm·rasPre로 적는다 — 꼬리부터 치환해 머리로 돌아오면 책의 (⋯(q/vₙ₋₁→eₙ₋₁)⋯)/v₀→e₀다.

힌트: 꼬리가 비면 AS 하나(Hoare.assign). 아니면 AS로 머리 대입을 올리고 — 사후조건은 바로 꼬리의 rasPre — SQ로 꼬리의 재귀 호출에 잇는다.

책은 RASₙ을 "건전할 뿐 아니라 완전하다"고 특별히 짚는다 — 결론이 타당하면 전제도 타당하다는 뜻이다. 그 완전성이 새 채점 연습 §3.3 ras-complete다(Derived.lean). ReynoldsTests/Ch03.lean이 책 p.61의 예 {y > 3} x := 2×y; x := x−y {x ≥ 4}를 Hoare.ras로 회귀 검사한다.

규칙마다 앞 장의 정리 하나🔗

건전성은 Hoare에 대한 구조적 귀납이다. AS·SQ·CD·WHP의 의미 판을 독립된 연습으로 증명하고, 아래 구문 판은 그 결과를 구문 단언에 적용하는 따름정리로 둔다.

대입 공리의 건전성은 1장 명제 1.4 그대로다. §1.4에서 포획을 피하는 치환을 애써 만든 것이 이 한 줄을 위해서였다.

while 규칙의 건전성은 §2.4의 Scott 귀납법이다. §3.1에서 본 두 사실, 곧 ⊥가 모든 사후조건을 만족한다는 것과 Sat이 극한을 통과한다는 것이 귀납의 두 의무를 채운다.

§2.5의 명제 2.6, 명제 2.7에 이어 Scott 귀납법을 세 번째로 쓰는 자리다. 앞의 둘은 두 상태 사이의 관계를 다뤘고 이번에는 한 상태의 술어라 더 단순하다.

Reynolds §3.5 pp.67–68의 DC는 s; v := e; c의 명세를 s; newvar v := e in c로 옮긴다. s는 비어 있을 수도 있는 앞부분이다. 두 명령은 같은 본체를 실행하며, 선언만 끝에서 지역 변수 값을 복원한다. 그래서 사후조건 q가 v를 보지 않으면 충분하다. 사전조건과 초기값 식에는 이 조건이 없다.

예를 들어 바깥 x = 3에서 newvar x := x + 1 in y := x는 y = 4를 남긴다. 초기값의 x는 바깥 값이다. 앞부분에서 x := 7을 실행했다면 본체는 y = 8을 만들고, 선언이 끝난 뒤의 x는 7이다. 앞부분을 실행하기 전의 3으로 복원하면 안 된다.

연습 3.9의 DC 건전성을 부분·전체 정확성 한 쌍으로 증명한다. hQ는 지역 변수의 값만 바꾸어도 사후조건의 진릿값이 같다는 뜻이다.

힌트: Comm.eval_seqs로 앞부분을 분리한다. 부분 정확성에서는 선언의 종료 결과를, 전체 정확성에서는 대입 판의 종료 결과를 출발점으로 삼는다. Flat.bind_eq_some_iff와 Flat.map_eq_some_iff로 중간 상태와 복원 전 상태를 찾는다.

RN은 결합 이름을 바꾸어도 뜻이 같다는 규칙이다. 여기서는 같은 앞부분 뒤의 지역 선언을 두 방향으로 바꾸는 Comm.PrefixRename을 사용한다. 초기값 e는 결합 범위 밖이므로 그대로 두며, 새 이름 w의 조건은 정확히 w ∉ FV(c) \ {v}다.

힌트: §2.5의 Comm.newvar_rename과 Comm.seqs_congr를 연결한다. 이 연습은 DC의 답을 사용하지 않는다.

책 p.68의 {x = 0} newvar x := 1 in x := x + 1 {x = 0}에는 DC를 바로 쓸 수 없다. 사후조건에 x가 있기 때문이다. 먼저 지역 이름을 y로 두고 DC를 적용한다. 그 명령을 RN으로 x로 바꾸면 바깥 x = 0을 유지하는 원래 명세를 얻는다. ReynoldsTests/Ch03.lean은 이 유도를 부분·전체 정확성에서 각각 검사한다.

책과의 차이: 책의 RN은 단언과 명령에서 여러 결합 이름을 바꾸는 일반 규칙이다. 여기서는 앞부분 뒤의 지역 선언에 한정한다. 여러 번의 명령 이름 바꾸기는 규칙을 반복 적용하고, 단언의 이름 바꾸기는 의미 함의인 결과 규칙으로 옮긴다.

기존 Hoare.newvar와 HoareT.newvar는 AS·SQ·DC로 유도한 제공 API다. 그 API의 세 신선함 조건은 검증 조건 생성기와 최약 사전조건 코드의 기존 사용을 보존한다. 직접 DC를 사용할 때는 사후조건의 조건만 필요하다.

절들을 모으면 건전성이다.

대입 공리는 왜 거꾸로인가🔗

{q/v→e} v := e {q}는 사후조건에서 출발한다. 앞으로 가는 판도 있다. Floyd의 판은 대입 전 값을 새 변수 v₀로 기억해 둔다.

이 판도 건전하다(보충). 신선함 조건이 셋 필요하다.