← 课程 形式化验证
0 / 5 单元
English
第 5 课

形式化验证：检查每一种情况，而不只是一部分

测试只试一部分输入，然后指望剩下的也没问题。形式化验证用数学和巧妙的搜索把所有输入都检查一遍。在这节课里，你会抓住一个测试漏掉的 bug，精确写下代码应该做什么，让计算机探索一个小程序的每一个状态，并证明一个循环是正确的。

形式化验证要证明的是：系统对每一个输入、或每一个可达状态都满足规约。手段有两类：穷举搜索（模型检测、SMT），或演绎证明（霍尔逻辑、证明助手）。它给出的保证，恰好和规约以及背后的假设一样强，不会更强。

第 1 单元

为什么光靠测试不够

这个 abs 函数永远不应该返回负数。它处理的是 8 位小整数，范围从 −128 到 127，一共只有 256 种可能的输入。先跑 100 个随机测试，再检查每一个输入。

同一个 abs，现在换成 16 位补码整数：65,536 个输入，恰好一个反例。比较随机测试和穷举检查，然后看看为什么穷举检查无法扩展，以及 SMT 求解器是怎么做的。

8 位整数的 abs
// 8 位有符号整数：-128 … 127
function abs(x) {
  if (x < 0) return -x;
  return x;
}
// 承诺：对每个 x，abs(x) >= 0
C，16 位
#include <stdint.h>

int16_t abs16(int16_t x) {
  return x < 0 ? (int16_t)-x : x;
}
// 性质：对所有 x，abs16(x) >= 0
已检查输入：0 · 发现失败：0
    未测试 通过 失败
    先跑随机测试。大多数测试套件就是这么做的。
    哪里出错了？ 8 位整数能存下 −128，却存不下 +128。所以 -(-128) 装不下，会回绕成 −128。256 个输入里只有 1 个会暴露这个 bug，所以随机测试通常会错过它。检查每一个输入则每次都能找到。真实程序的输入多到不可能逐个尝试，所以验证工具会一次性推理所有输入。

    穷举检查无法扩展

    以每秒十亿次检查的速度，试遍所有输入需要的时间：

    输入数量时间
    一个 int8256不到 1 µs
    一个 int1665,536约 66 µs
    一个 int324.3 × 10⁹约 4.3 秒
    一个 int641.8 × 10¹⁹约 585 年
    两个 int643.4 × 10³⁸约 10²² 年
    SMT-LIB：是否存在 x 使 abs(x) < 0？
    (declare-const x (_ BitVec 32))
(define-fun abs32 ((v (_ BitVec 32))) (_ BitVec 32)
  (ite (bvslt v #x00000000) (bvneg v) v))
(assert (bvslt (abs32 x) #x00000000))
(check-sat)   ; sat
(get-model)   ; x = #x80000000  (-2147483648)
    符号推理，而不是逐个枚举。 SMT 求解器拿到的是性质的否定，形式是一个位向量公式。它不会一个一个地试输入，而是传播约束、从冲突中学习、拆分情况，最后回答：
    • sat，并给出一个模型：一个具体的反例，这里是 x = INT_MIN。
    • unsat：没有任何输入违反该性质。这就是对全部 2³² 个输入的证明。加上前置条件 x != INT_MIN，查询结果就变成 unsat。
    在 C 语言里，对 32 位 int 的 INT_MIN 求 -x 是未定义行为，比算错还糟。同类 bug 曾在 Java 标准库二分查找的 (low + high) / 2 里藏了好多年，直到数组长度超过 2³⁰ 才暴露出来。
    第 2 单元

    规约：把“正确”的含义说清楚

    要检查一个程序，首先得写下它应该做什么。这就是规约（specification）。这里的任务是给一列数排序。勾选你想要求的规则，检查器会试遍所有短列表，并告诉你四个程序中哪些仍然通过。

    规约是一组关于输入和输出的后置条件（以及前置条件）。一条子句一条子句地构建 Sort 的规约。有界检查器会在 {0, 1, 2} 上长度为 0 到 4 的每个列表（共 121 个输入）上运行每个实现，并对每组子句报告第一个反例。

    规约：输出必须……
    候选程序
    用 Dafny 风格语法写出的规约
    
    
    

    
    
      三种规则
      
      
        
    • 前置条件：代码运行之前必须成立的事情。例如：取第一个元素之前，“列表不为空”。
      • 
        
    • 后置条件：代码结束时承诺成立的事情。例如：“结果是有序的”。
      • 
        
    • 不变式：始终保持成立的事情。例如：“账户余额永远不为负”。
      • 
      
    
      太弱的规约会放过错误的程序，比如那个总是返回空列表的程序。验证能证明代码符合规约，却无法告诉你这份规约是不是你真正想要的。
    
    
    
    
      
    
        
    
          
    前置条件：requires
    
          
    method BinarySearch(a: seq<int>, key: int) returns (i: int)
  requires forall p, q :: 0 <= p < q < |a| ==> a[p] <= a[q]
  ensures 0 <= i ==> i < |a| && a[i] == key
  ensures i < 0 ==> key !in a
    
        
    
        
    
          谁负责证明什么
          
      
            
    • requires 是每个调用者的义务。在方法内部，它是一个假设。
      • 
            
    • ensures 是方法体的义务，调用者可以依赖它。
      • 
            
    • 类不变式或循环不变式必须在规定的位置成立（方法进入和退出时、每次循环迭代时）。
      • 
            
    • 上面这种有界检查不是证明。它依赖“小范围假设”：大多数 bug 在小输入上就会出现。像 Dafny 这样的验证器能对任意长度的列表证明这些子句。
      • 
          
    
        
    
      
    
    
    
  
    

  
  
    
    
    第 3 单元
    
    
    模型检测：探索每一个状态
    
    
    两个程序共用一台打印机，同一时间只能有一个在打印：这段代码叫做临界区。每个程序都有一面旗子，举起来表示“我想进去”。模型检测器会尝试两个程序执行步骤的每一种可能顺序，寻找坏状态。
    
    
    两个进程、共享的旗子和一条互斥性质。检测器在交错语义上做广度优先搜索：一个状态是 (pc₀, pc₁, flag₀, flag₁, turn)，每条迁移是某个进程的一个原子步骤。它在每个可达状态上检查不变式，并寻找死锁。
    

    
    
    
    
      
    
        
    
        
    
      
    
      
    
        
    
        
    
          
        
    
        
    找到的状态：0 · 坏状态：0 · 死锁：0
    
      
    
    
    

    
    
    
    
      起点
      两个都在临界区
      死锁
      反例路径
    
    
    
    点“探索每一个状态”。
    

    

    
    
      为什么不直接测试？ 只有当两个程序几乎同时检查旗子时，这个 bug 才会出现。在真实测试中这种时机很少见，所以 bug 可能在成千上万次运行中都溜过去。模型检测器不靠运气：它访问每一个可达状态，所以只要坏状态存在就一定能找到，还会告诉你到达那里的确切步骤。代价是它检查的是程序的模型，而模型可能省略了真实程序的一些细节。
    
    
    
    
      
    
        
    
          
    状态爆炸
    
          
    这里每个进程有 4 个位置。还没算共享变量，N 个进程就最多有 4N 种组合：
    
          
    
            
    
              
    进程数位置组合数
    
              
                
    216
    
                
    4256
    
                
    865,536
    
                
    164.3 × 10⁹
    
                
    321.8 × 10¹⁹
    
                  
            
    
          
    
          
    真正的检测器用这些办法对抗状态爆炸：偏序归约（跳过独立步骤的不同排列）、对称性归约、符号表示（BDD），以及基于 SAT/SMT 的有界模型检测，它检查不超过 k 步的所有运行。
    
          
    安全性与活性
    
          
      
            
    • 安全性：坏事永远不会发生。“永远不会两个都在临界区。”违反它的证据是一条通向坏状态的有限轨迹。
      • 
            
    • 活性：好事最终会发生。“想进入的进程最终能进入。”违反它的证据是一次无限运行，表现为套索形：一条路径进入一个永远到不了好状态的环。检查活性需要公平性假设，否则一个从不调度某个进程的调度器会让任何进程“饿死”。
      • 
            
    • “先举旗”协议是安全的，但可能死锁：两面旗子都举着，两个进程永远互相等待。没有死锁是活性的必要条件，但还不够。Peterson 算法在弱公平性下还能保证不会饿死。
      • 
          
    
        
    
        
    
          
    TLA+ 写的 Peterson（用 TLC 检查）
    
          
    ---- MODULE Peterson ----
VARIABLES pc, flag, turn
vars == <<pc, flag, turn>>
Other(i) == 1 - i

Init == /\ pc = [i \in {0, 1} |-> "idle"]
        /\ flag = [i \in {0, 1} |-> FALSE]
        /\ turn = 0

Raise(i) == /\ pc[i] = "idle"
            /\ flag' = [flag EXCEPT ![i] = TRUE]
            /\ pc' = [pc EXCEPT ![i] = "turn"]
            /\ UNCHANGED turn
Yield(i) == /\ pc[i] = "turn"
            /\ turn' = Other(i)
            /\ pc' = [pc EXCEPT ![i] = "wait"]
            /\ UNCHANGED flag
Enter(i) == /\ pc[i] = "wait"
            /\ (~flag[Other(i)] \/ turn = i)
            /\ pc' = [pc EXCEPT ![i] = "crit"]
            /\ UNCHANGED <<flag, turn>>
Leave(i) == /\ pc[i] = "crit"
            /\ flag' = [flag EXCEPT ![i] = FALSE]
            /\ pc' = [pc EXCEPT ![i] = "idle"]
            /\ UNCHANGED turn

Proc(i) == Yield(i) \/ Enter(i) \/ Leave(i)
Next == \E i \in {0, 1} : Raise(i) \/ Proc(i)
Spec == Init /\ [][Next]_vars
             /\ \A i \in {0, 1} : WF_vars(Proc(i))

MutualExclusion ==                \* 安全性
  ~(pc[0] = "crit" /\ pc[1] = "crit")
NoStarvation ==                   \* 活性
  \A i \in {0, 1} : pc[i] = "turn" ~> pc[i] = "crit"
====
    
        
    
      
    
    
    
  
    

  
  
    
    
    第 4 单元
    
    
    证明循环是正确的
    
    
    模型检测器需要一个小的、有限的世界。要证明代码对任意输入都正确，我们得靠推理。循环是最难的部分，诀窍是循环不变式：每次循环准备检查条件时都成立的一个事实。先运行下面的循环，再选出能证明它正确求和的不变式。
    
    
    霍尔逻辑证明的是三元组 {P} S {Q}。对一个循环，你要给出不变式 I，完成三个验证条件，再给出一个变式来证明终止。运行用反复减法实现的整数除法，然后选出 I 和变式。每条证明义务都在 n ≤ 12、d ≤ 4 以及较小的 q、r 的所有状态上检查；像 Dafny 这样的验证器会借助 SMT 求解器对所有整数证明它们。
    

    
    
      
    
        
    
        
    
      
    
      
    
        
    运行它
    
        
    
        
    
        
    
          
          
        
    
      
    
    
    
    
    
    
    

    
    哪个不变式能证明它？
    
    
    
    
    
    
    

    
    
      
    终止性：选一个变式
    
      
    部分正确性说的是“如果循环停下，结果就是对的”。要得到完全正确性，需要给出一个整数表达式：循环运行时它永远不为负，并且每次迭代都严格变小。它不可能无限地变小下去，所以循环一定会停。
    
      
    
      
    
    
    

    
    
      任何循环不变式都要回答的三个问题
      
      
        
    • 它在一开始、第一次迭代之前成立吗？
      • 
        
    • 如果它在某次迭代之前成立，那么这次迭代之后它还成立吗？
      • 
        
    • 当循环停下时，不变式加上“条件现在为假”，能得出我们承诺的结果吗？
      • 
      
    
      如果三条都成立，循环就对每一个可能的列表都正确，而不只是你跑过的那一个。像 Dafny 这样的工具会让计算机替你检查这三个问题。
    
    
    
    
      
    
        证明义务的形式化表述
        
      
          
    • 初始化：{P} init {I}。前置条件和初始赋值建立 I。
      • 
          
    • 保持性：{I ∧ B} body {I}。从任何满足 I 和守卫 B 的状态出发，执行一次迭代后仍满足 I。
      • 
          
    • 退出：I ∧ ¬B ⇒ Q。I 加上守卫的否定，推出后置条件。
      • 
          
    • 终止：I ∧ B ⇒ V ≥ 0，并且 {I ∧ B ∧ V = V₀} body {V < V₀}。
      • 
        
    
        保持性要对每一个满足 I ∧ B 的状态检查，而不只是程序实际到达的状态。这就是为什么像 q * d <= n 这样成立却太弱的不变式会失败：它说的信息不够，撑不过一步。加强不变式，正是日常证明工作的主要内容。
      
    
      
    各种工具的定位
    
      
    
        
    Dafny、Why3、Verus、SPARK在代码里写 requires、ensures 和不变式。验证器把它们转换成交给 SMT 求解器（Z3、cvc5）的条件。基本自动。
    
        
    Lean、Coq（Rocq）、Isabelle/HOL交互式证明助手。证明由你来写，由一个小而可信的内核检查。能力最强，但工作量大得多。
    
        
    TLA+、Alloy、SPIN、NuSMV把设计描述成状态和迁移，然后做模型检测。在代码写出来之前就能发现协议 bug。TLAPS 还能证明 TLA+ 规约。
    
        
    CBMC、Kani、KLEE对真实的 C、Rust 或 LLVM 代码做有界模型检测和符号执行，范围以循环展开的上限为界。
    
      
    
      
    在现实世界中
    
      
      
        
    • seL4：一个微内核，它的 C 代码在 Isabelle/HOL 中被证明实现了其抽象规约，在此之上还证明了安全性质。证明假设编译器、启动代码和硬件是正确的；后续工作还检查了编译出的二进制代码。
      • 
        
    • CompCert：一个在 Coq 中被证明会保持所编译程序语义的 C 编译器。研究人员用数以百万计的随机程序测试许多编译器时，在 CompCert 经过验证的部分没有发现生成错误代码的 bug，只在未经验证的前端里发现了。
      • 
        
    • AWS：从 2011 年起，工程师就在 S3、DynamoDB 等系统上使用 TLA+。模型检测发现了一些微妙的设计 bug，需要几十步的轨迹才能触发，测试和代码审查都漏掉了它们。
      • 
      
    
    
    
  
    

  
  
    
    
    第 5 单元
    
    
    自我检测