状态与转移
States and Transitions状态机说白了就是第四章的二元关系再加两个名字：元素叫状态（state），关系叫转移（transition），外加一个指定的起始状态。99 计数器：状态 0…99 与 overflow，0 → 1 → 2 → ⋯ → 99 → overflow。程序 = 状态机；飞机高度、核反应堆温度、web 服务器负载，凡"一步步走"的过程皆可建模。
第 2 章良序原理说过：给每步赋一个严格变小的良序值 ⇒ 过程必然停机。本章的主角是另一半：给每步找一个"保持不变"的性质 ⇒ 它永远成立。
不变量原理
The Invariant Principle一台机器人从原点出发，在无限网格上只能走对角线（(m,n) → (m±1, n±1)）。它能到达 (1,0) 吗？玩玩就知道——注意格子按 m+n 的奇偶染了色，机器人每走一步……
若 P 是状态机的保持不变量（preserved invariant）——起始状态满足 P，且每条转移 q → r 都有 P(q) ⇒ P(r)——则 P 对一切可达状态成立。
它就是归纳原理换了身衣服：起始状态真 = 基例；保持 = 归纳步。提出者是 Robert W. Floyd（1967），后来拿了图灵奖。顺便看一个反向陷阱：“保持”只约束满足 P 的状态的出边（P(q) ⇒ P(r)），对违反 P 的状态的出边没有任何承诺——所以保持不变量的否定不一定是保持不变量。真实反例见下节“永恒版”水壶：保持不变量 P ::= “两壶水量都是 3 的倍数”，但违反 P 的状态 (5,0) 经“灌满大壶”转移到满足 P 的 (9,0)，P 的否定就此失守。
虎胆龙威水壶
The Die Hard ExampleSimon 放了炸弹：一个 5 加仑壶、一个 3 加仑壶，要你精确量出 4 加仑放在秤上。状态 = (大壶水量 b, 小壶水量 l)，六种操作：灌满任一壶、倒空任一壶、互相倾倒。这台机器是非确定性的——同一状态有多种走法。原书证 (4,3) 可达（电影里拆弹成功），而换 9 加仑壶的《Die Hard Permanently》里 (4,l) 永不可达——不变量：所有可达水量都是 3 的倍数。亲手玩：
部分正确性与终止
Partial Correctness & TerminationFloyd 区分了验证程序的两大性质：部分正确性——"如果程序停了，结果是正确的"；终止性——"程序确实会停"。前者用不变量原理证（找出每步保持的断言），后者用良序原理证（找一个严格递减的非负整数派生变量）。原书的例子是快速幂：寄存器 x, y, z 从 (a, 1, b) 出发，z 减半、x 平方、视奇偶把 x 乘进 y，z = 0 时返回 y——不变量 y · xᶻ = a^b 每步保持，z 严格递减必到 0。
稳定婚姻问题
The Stable Marriage Problemn 位男士、n 位女士，每人心里有一份对异性的完整偏好排序。要给所有人配对，且配对稳定（stable）：不存在"两人都更爱对方而非现任配偶"的流氓对（rogue couple）。原书用 Brad / Angelina / Jennifer / Billy Bob 举例：Brad 和 Angelina 互为最爱却各配他人——婚姻岌岌可危。
Mating Ritual（相亲仪式）：每天早上，单身男士向自己名单上排位最高的女士唱小夜曲；下午，每位女士从追求者中留下最爱、对其余宣布"此生休想"；晚上，被拒男士把该女士划掉。直到每位女士都恰有一位追求者，全员成婚。三大定理：必在 n² 天内终止；人人结婚；结果稳定。还有一记反转：这套仪式对男士最优、对女士最劣（定理 6.4.9）——虽然看起来天天挑人的是女士。
习题实战：派生变量与可达性
6.3 & 6.2.3, Playable6.3 的派生变量判定 + 6.2.3 的水壶可达性计算器。
终局自测
Final Check六题，覆盖全章。
彩蛋与课后挑战
Easter Eggs & ProblemsRobert W. Floyd：没读过博士的图灵奖得主（原书 6.2.2 侧栏）
不变量原理由 Floyd 于 1967 年在卡内基理工提出。他十几岁就被博士班录取，却考试挂科退学、再没回去——照样当上教授，后来以形式文法与程序验证的奠基工作获图灵奖。作者 Meyer 回忆：Floyd 兴冲冲讲不变量原理时，Meyer 心想"这么显然的东西也值得兴奋？"后来才懂：Floyd 兴奋的不是定理之真，而是如此简单的方法竟能如此广泛地验证程序。
Akamai 的相亲仪式（原书 6.4.1 侧栏）
本章作者之一 Tom Leighton 联合创办的 Akamai（全球最大 CDN 之一，6.5 万+ 服务器、日均 8000 亿+ 请求）真的把 Mating Ritual 的变体用于流量分配：web 请求扮演"女士"（按延迟与丢包挑服务器），服务器扮演"男士"（按带宽成本挑请求）——6.042 的定理在为你加载网页。
东南跳跃机器人（原书 6.3.4，可选）
机器人每次要么向西一格，要么向南一格加任意远向东跳。它能停在原点，但无法用非负整数派生变量证终止——因为它可以拖任意多步。妙招：定义派生变量 v(x,y) = y + x/(x+1)，取值在良序集 ℕ+𝔽（第 2 章埋的伏笔！）上严格递减——定理 6.3.3（良序集版终止定理）接管。第 2、5、6 章在此会师。
课后挑战（均出自原书习题）
- 6.6 精确证明快速幂至多 2(⌈log₂b⌉+1) 次乘法。
- 附加题（经典，原书未收）九枚金币一枚假（偏轻），天平最少称两次——用不变量思路写出状态机与策略。
- 6.23 构造一份四人偏好，使"同性 buddy 配对"不存在稳定匹配——异性版的定理在同性场景失效。
- 附加题 证明 Mating Ritual 里男士的最优配偶可能不止一个可行配偶的情形分析（feasible spouse 定义 6.4.5）。