3장 명세와 그 증명🔗

1장은 단언이 언제 참인지를 정했고, 2장은 명령이 무엇을 하는지를 정했다. 3장은 둘을 잇는다. 명령 앞뒤에 단언을 놓아 "이런 상태에서 시작하면 저런 상태로 끝난다"를 말하고, 그런 주장을 증명하는 규칙을 세운다. Hoare 논리다.

이 장은 새 대상을 거의 만들지 않는다. 명세의 뜻은 2장의 Comm.eval 위에 정의하고, 규칙의 건전성은 1·2장의 정리로 증명한다. 앞의 두 장에서 쌓은 것이 여기서 한꺼번에 쓰인다.

1. 이 장에서 배우는 것
2. 앞 장의 정리가 쓰이는 곳
3. 읽는 순서
4. §3.1 명세의 구문과 뜻
5. §3.2~3.5 추론 규칙과 건전성
6. 보충 주석 명세 · §3.4 전체 정확성
7. §3.3·§3.5 유도 규칙과 보충 규칙
8. §3.6~3.7 예제
9. §3.8 복잡한 점과 한계
10. 보충 — 최약 사전조건과 완전성