이 장에서 배우는 것🔗

• 부분 정확성과 전체 정확성 — 발산을 어떻게 세느냐가 두 명세의 유일한 차이다

• 건전성 — 규칙마다 앞 장의 정리 하나가 받친다. 대입 공리는 명제 1.4, while 규칙은 Scott 귀납법, 변수 선언 규칙은 명제 1.1이다

• 불변식과 변항 — 반복을 증명할 때 사람이 골라야 하는 두 가지

• 검증 조건 — 주석 명세에서 확인할 함의들을 기계적으로 뽑아 내는 방법

• 상대 완전성 — 단언의 타당성을 오라클로 두면 타당한 명세가 모두 유도된다는 것, 그리고 그 "조건부"가 어디서 오는지