주석 명령🔗

사람이 적어야 하는 것만 붙인 구문을 둔다. 주석을 지우면 명령이 된다.

검증 조건 생성기🔗

사후조건에서 뒤로 가며 사전조건을 계산하고, 도중에 확인해야 할 함의들을 모은다. 대입 공리가 거꾸로 가기 때문에 계산도 거꾸로 간다.

대입

사후조건에 치환을 건다. 확인할 것은 없다.

순차 합성

이음매 r이 뒤쪽 명령의 사전조건보다 강해야 한다. 이것이 검증 조건 하나다.

조건

(b ⇒ p₀) ∧ (¬b ⇒ p₁). 확인할 것은 없다.

반복

사전조건은 불변식이다. i ∧ b가 본체의 사전조건보다 강한지, i ∧ ¬b가 사후조건보다 강한지를 확인해야 한다.

변수 선언

∀ v. v = e ⇒ p. 결합자를 ∀로 가두면 바깥 단언에 새지 않는다.

검증 조건이 전부 타당하면 Hoare 유도가 있다(Annot.vcg_sound). Dafny나 Why3 같은 검증 도구가 하는 일의 축소판이다. 맞바꾸기에 주석을 달면 남는 일은 치환을 펼치는 것뿐이다.

전체 정확성 — 변항🔗

전체 정확성 체계는 반복에 WHT를, 상수 규칙에 종료 전제가 있는 CST를 쓴다. 반복이 끝난다는 것을 말하려면 한 바퀴마다 줄어드는 양, 곧 변항(variant)이 있어야 한다.

z는 본체 실행 전의 e 값을 기억하는 유령 변수다. 명세에는 나오지만 명령에는 자유롭게 나오지 않는다. z ∉ FV(c)는 본체가 이 값을 보존한다는 사실뿐 아니라, z를 바꾼 입력에서의 실행 결과를 원래 입력으로 옮기는 데도 쓰인다. 값의 보존만 말할 때는 더 약한 z ∉ FA(c)로 충분하다.

§3.1에서 보았듯 전체 정확성은 극한을 통과하지만, ⊥에서 종료를 보일 수 없어 Scott 귀납법의 시작 조건이 막힌다. 그래서 건전성 증명은 측도 위의 정초 귀납을 쓴다. 2장에서 구체적인 루프의 값을 계산할 때 손으로 잡던 측도를 이제는 규칙이 인자로 받는다.

의미 단언에서는 실행 전 변항 값을 n : Int로 기억한다. 연습에서는 변항보다 큰 자연수 상계를 줄이는 귀납법을 구성한다. 비음수 조건은 반복 조건이 참일 때만 필요하므로, 마지막 본체 실행이 변항을 음수로 만들어도 다음 조건이 거짓이면 된다.

구문 판 whT_sound는 책 p64의 유령 변수 규칙을 그대로 유지하는 제공 정리다. 본체를 σ[z := n]에서 실행한 뒤, 명제 2.6으로 z 밖의 결과를 원래 입력의 실행에 옮긴다. 이 과정은 의미 규칙에 줄 전제를 만들며, 반복의 종료는 위 연습이 증명한다.

명제 2.6의 두 반쪽이 모두 쓰인다. (b)는 본체가 z를 건드리지 않음을, (a)는 z만 다른 두 시작 상태에서 본체의 결과가 불변식과 변항이 보는 변수들 위에서 같음을 준다.

§2.8의 백까지 세기를 규칙만으로 유도하면, 이번에는 끝난다는 것까지 얻는다.