읽는 순서🔗

1. Spec.lean — §3.1 명세의 뜻, (보충) 순서로 본 명세

2. Hoare.lean — §3.2~3.5 추론 규칙

3. Soundness.lean — 규칙마다 건전성

4. Assign.lean — §3.3 대입 공리의 방향, (보충) Floyd의 앞으로 가는 판

5. Annot.lean — (보충) 주석 명세와 검증 조건, §3.4 전체 정확성의 while 규칙

6. Total.lean — §3.4 전체 정확성의 while 규칙

7. Derived.lean — §3.3·§3.5 유도 규칙(ISK·MSQₙ·RASₙ), 구조 규칙, (보충) ∃·치환 규칙

8. Semantic.lean — 의미 단언 위의 규칙

9. Examples/Fib.lean, Examples/FastExp.lean — §3.6, §3.7 예제

10. Wlp.lean — (보충) 최약 사전조건과 완전성

전부 Reynolds/Answers/Ch03/ 아래에 있고, Reynolds/Exercises/Ch03/에는 같은 선언 순서에서 채울 자리만 sorry로 비어 있다. Exercises 트리는 앞 장의 완성본을 가져다 쓰므로 1·2장을 풀지 않아도 3장을 풀 수 있다.

책 §3.8(pp.74–76)의 실제 한계는 복잡한 점과 한계에서 읽는다. 유령 변수와 산술·오류 모델의 경계를 다루며, 최약 사전조건과 완전성은 별도 보충 주제다.