形式证道

Dijkstra 1970 年的名言是本章地基：「测试只能证明 bug 的存在，不能证明 bug 的不存在。」形式化方法负责补上后半句：用数学写清系统该做什么（规约 specification）与实现做了什么（模型/代码），再证明两者等价——覆盖所有输入、所有状态、所有路径。两件套缺一不可：只有规约没有证明是写文档，只有模型没有规约是无的放矢。台上五份案卷各漏一处：Therac-25 的并发竞态、Ariane 5 的 64 位转 16 位溢出、FDIV 的查表缺陷、Knight 的死代码、737 MAX 的单点失效——共性是测试只采样了输入空间的一角，而 bug 恰在没采样的角落。形式化不是「更狠的测试」：它换了数学基础——从「观察若干样本归纳」换成「对全空间演绎」。代价也随之而来：建模成本高、规约必须精确，这笔账记在 K25-15。

命题逻辑：原子命题 + 连接词 ¬、∧、∨、→、↔，语义就是真值表——石壁上那四行。蕴含 P→Q 只在 P 真且 Q 假时为假；P 假时恒真，即「空虚真」（vacuous truth）：没下雨，「下雨则地湿」没有被违反。谓词逻辑再加三样：项、谓词、量词（∀/∃）——表达能力从「命题之间的关系」升到「对象之间的关系」，这才够写程序性质：「∀x∈N, x+1>x」就是谓词逻辑公式，一个反例即推翻。判定性分野：命题逻辑的可满足性（SAT）是 NP 完全但可判定；一阶逻辑的有效性不可判定（丘奇定理，1936）——这是验证工具链必须绕行的暗礁（详见 K25-14）。台上量词题选 ∀ 的理由：x+1>x 对每个自然数都成立，逐个验证不可能，只能全称量化。

Clarke、Emerson、Sifakis 在 1981 年前后各自奠基，2007 年同获图灵奖。三步走：①建模——系统抽象成 Kripke 结构（状态集 + 转移关系 + 原子命题标记）；②规约——性质写成时序逻辑公式；③验证——检查系统所有行为是否满足公式。与定理证明的根本区别是全自动：不需要人会写证明，工具自己遍历；性质被违反时还能吐出反例（counterexample）——一条具体的状态路径，直接可当调试线索。指数来源就在台上：n 个布尔变量，每个状态是变量的一组赋值，共 2^n 个——3 个变量 8 个状态只是起点，每加一个变量翻一倍。模型检验的哲学是「穷举但有反例」，定理证明的哲学是「推理但费人力」——本章两幕主线在这里分岔。

程序的性质很少是「现在的」，多是「永远/最终/直到」——时序性质。LTL（线性时序逻辑）沿单条执行路径解释，四个基本算子：X（下一刻）、F（最终◇）、G（总是□）、U（直到）；G(req→F ack) 读作「任何时刻的请求，之后总会被响应」。CTL（计算树逻辑）站在分支点看，加路径量词 A（所有路径）/E（存在路径），与算子成对组合：AG、EF、AU……AG(req→AF ack) 语义与上句相同。两者表达能力互不包含（CTL* 才统一两者）；工具跟着走：SPIN 收 LTL——公式转 Büchi 自动机，与系统做积自动机查空；NuSMV 收 CTL——在 BDD 上算不动点。分叉镜的寓意：自然语言的「最终」在 LTL/CTL 里是两个不同的公式——模糊的规格就是 bug 的入口。

SPIN（Simple Promela INterpreter，Holzmann，Bell Labs）：建模语言 Promela（进程 + 消息通道），引擎是 on-the-fly 深度优先——状态边生成边查、不必先建整张图，配偏序归约压状态；用它验证过网络协议与教科书互斥协议，台上那条 LTL 活性公式跑出反例时给出的就是一条「请求后永远等下去」的路径。NuSMV（CMU SMV 的开源重构）：语言是模块化状态机，主武器是符号模型检验——BDD 上算不动点，一条 CTL 公式 AG¬(p1.cs∧p2.cs) 就验掉互斥安全性。工程分工经验法则：并发/网络协议 → SPIN；同步硬件与控制状态机 → NuSMV。两者共享模型检验的宿命：状态空间一大，就得回到 S5 的账上。

FDIV 案卷的解剖：Pentium 的 SRT 除法器用查表实现，2048 个表项里有 5 个本应为零的槽位没有正确写入——除数恰好落进这些槽位时，结果从第 4~5 位有效数字开始出错。Intel 耗资 4.75 亿美元全量召回，震动之后硬件成为形式化第一个大规模落地领域：SRT 查表恰是模型检验的理想对象——状态空间规整、规约清晰（IEEE 754 给每一位都下了定义）。此后 Intel/IBM 的浮点单元普遍经过模型检验，「形式化验证浮点单元」成了设计流程的标准操作；等价性检查（证明优化前后电路等价）更是芯片签核流程的一部分。硬件先于软件落地，不是因为硬件更容易，而是硬件的失效成本立即兑现——4.75 亿美元学费买来整个行业的转向。

先算账：2^265≈10^80——265 个变量的状态数等于宇宙原子总数；100 个变量遍历约 4×10^13 年，宇宙年龄的约 3000 倍。缓解四法对应台上四张卡：①BDD（二元决策图，Bryant 1986）：布尔函数表示成有向无环图、同构子图共享——McMillan 的 SMV 借它把可验证规模推到 10^120 状态量级（Huth & Ryan 的教材口径），「符号模型检验」由此得名；②抽象（abstraction/refinement）：把与性质无关的变量抽象掉，在更小的空间验证，反例可疑再细化（CEGAR 循环）；③POR（偏序归约）：并发系统里交换两个独立事件的顺序不改变性质——只探索真正不同的交错序；④SAT/BMC（有界模型检验，Biere 1999）：把「前 k 步内是否违反」编码成 SAT 实例，找反例极快。四法都在压 2^n，但没有一法把它变成多项式——指数本质不灭，这是所有模型检验器的天花板。

换路：不遍历状态，用公理 + 推理规则做演绎。核心规则就一条——肯定前件（modus ponens）：有 P 和 P→Q 即得 Q；配上数学归纳法，「对任意 n」的证明有了杠杆——这正是「证明所有路都通向同一结论」的含义。四色定理是分水岭：1976 年 Appel 与 Haken 用程序枚举 1936 种不可约构形完成证明，人工无法复核——「计算机证明算不算证明」吵了三十年；2005 年 Gonthier 用 Coq 把整个证明形式化，机器内核逐行检验，争议就此终结。定理证明的真正卖点不是快，是「小内核」（de Bruijn 准则）：几千行经过审计的内核可以检验任意长的证明——把信任压缩到一个可读的小核上。证明可以机器辅助生成，但检验只认内核。

三大家谱。Coq（法国 INRIA，归纳构造演算内核）：代表作 CompCert——Leroy 团队证明了 C 编译器每一步优化的语义忠实，编译器 bug 从此不用背锅。Isabelle/HOL（高阶逻辑 + LCF 小内核架构）：代表作 seL4——2009 年第一个获得完整功能正确性证明的 OS 微内核，Isabelle 证明代码数十万行、远超内核本身。Lean（de Moura 2013）：定理证明与编程一体，mathlib 已是百万行级数学库，陶哲轩用它推动主流数学形式化。工作模式都是「人给战术（tactic），机器做归约」：输入 intros、induction、simpl，proof state 实时刷新，QED 时内核独立检验——构造与检验分离，人管战略，机器管战役与审计。台上 Coq 终端那几条命令，就是这个循环的最小演示。

Hoare 1969。三元组 {P}S{Q}：若执行前 P 成立且 S 终止，则执行后 Q 成立。各语句的公理：赋值最反直觉——{Q[E/x]} x:=E {Q}，证明要倒着推；顺序复合与条件各配一条规则。循环是难点：要找不变式 I，尽三重义务——①入口成立；②保持（I ∧ 循环体 ⊢ I'）；③退出推 Q（I ∧ ¬cond ⊢ Q）。台上例题：{x=0 ∧ i=0} while (i<n) {i++; x++} {x=n}，正确不变式是 x=i——入口 0=0、保持 x=i→x+1=i+1、退出 i=n 得 x=n；而 x≤n、x≥0 两条「看起来也对」的候选都在第三重义务上失败（推不出 x=n）。找不变式没有算法——本质上它就是证明，受 K25-14 的不可判定性约束；Dafny 能自动检验不变式，但找，还得靠人。

三件套各守一段。Dafny（微软研究院，Leino）：语言级集成——前置条件 requires、后置条件 ensures、循环不变式 invariant 直接写进代码，编译时调 Z3 SMT 求解器消化证明义务，违反时给出具体反例输入，「注解即定理」。Frama-C（法国 CEA）：面向 C 遗产代码——ACSL 注解写规格，WP 插件把每条注解变成证明义务，交给 SMT 求解器或 Coq。TLA+（Lamport，2013 图灵奖得主）：验证的不是代码是设计——时态动作逻辑写分布式协议规约，TLC 模型检验器查错；AWS 是最大工业用户，用 TLA+ 验证 S3、DynamoDB 等关键服务（CACM 2015 记载其找到了海量测试多年未发现的复制 bug）。共同内核：都是「规约 + 自动消化证明义务」——Hoare 规则被 SMT 求解器批量执行了。

镜子两面的对应表：命题↔类型、证明↔程序、证明化简↔求值——台上五张配对卡就是这张表。细看：P∧Q↔积类型 A×B（证明对）；P∨Q↔和类型 A+B；P→Q↔函数 A→B（证明变换器）。依赖类型把量词也收进来：∀x.P(x)↔Π 类型（依赖函数），∃x.P(x)↔Σ 类型（依赖对）——Lean 终端里 (h : xs.length>0) 把前提作为参数写进类型，Vector α n 把长度编进类型。两个推论：①强归一化——每个良类型的项都终止，故对应逻辑一致，Coq/Lean 不会证出假命题；②它对应直觉主义逻辑——排中律不是定理（古典逻辑要加 call/cc 类控制算子才进得来）。实践意义：类型检查即证明检验——你写的每行带类型代码都是证明的碎片，类型系统越强，碎片越大。

图灵 1936 的自指陷阱（台上六步推导）：假设 H(P,x) 能判定停机；构造 D(x)=若 H(x,x) 则死循环否则停机；问 D(D)——两个分支都矛盾，故 H 不存在。停机问题不可判定。归约是主武器：停机⟶程序等价性⟶Rice 定理——程序的一切非平凡语义性质（关乎功能而非语法）都不可判定，连「这个函数是否总返回偶数」也不可判定。对形式化的意义：不存在验证一切的全自动机器——定理证明器必须人机协作（K25-08）、模型检验器必须限系统为有限状态（K25-03）、SMT 求解器只工作在可判定理论片段（线性算术、数组、位向量）。边界之内效率仍有天壤：素性判定（AKS）多项式时间可判定，SAT 是 NP 完全但现代求解器极强——不可判定是悬崖，可判定与高效之间是整个工程的地带。