[] 用测试对照证明

  • Glomzzz
  • 2026-10-10
  • About

纸面证明可能写错，代码也可能和规则对不上。定理本身可以直接写成测试：生成大量项，拿定理的结论去检查。

#[test]
fn safety() {
    for t in corpus() {                        // 深度 ≤ 2 的全部项 + 随机的深项
        let Some(ty) = type_of(&t) else { continue };
        let mut cur = t.clone();
        loop {
            // 进展：不是值，就必须能归约
            let Some(next) = step(&cur) else {
                assert!(is_value(&cur), "受阻了：{cur:?}");
                break;
            };
            // 保型：一步归约，类型不变
            assert_eq!(type_of(&next), Some(ty), "{cur:?} ⟶ {next:?}");
            cur = next;
        }
    }
}
#[test]
fn safety() {
    for t in corpus() {                        // 深度 ≤ 2 的全部项 + 随机的深项
        let Some(ty) = type_of(&t) else { continue };
        let mut cur = t.clone();
        loop {
            // 进展：不是值，就必须能归约
            let Some(next) = step(&cur) else {
                assert!(is_value(&cur), "受阻了：{cur:?}");
                break;
            };
            // 保型：一步归约，类型不变
            assert_eq!(type_of(&next), Some(ty), "{cur:?} ⟶ {next:?}");
            cur = next;
        }
    }
}

这门语言没有循环，每一步都让项变小，所以 loop loop 一定会停。代码在 code/plt-arith code/plt-arith 下， cargo test --release cargo test --release 即可运行。样本是深度 2 以内的全部 59439 个项，外加 50000 个深度到 6 的确定性随机项。

确定性也能这样测。测试里把 E-规则逐条照抄成一个返回所有可能 𝑡 ′ 的函数，不做任何排序或排除，然后检查它在每个样本上至多给出一个结果，并且和 step step 一致。这同时验证了 [附注] 分支顺序里藏着证明 的说法： match match 的分支顺序没有偷偷改变语义。

前文提过的两个错误写法都会被抓住，但抓住它们的测试不同：

  • T-If 不检查 else 分支，破坏的是保型。 safety safety 实际报出的反例是 succ ( if  false  then 0 else  true )：错误的检查器只看 then 分支，认为它是 Nat；一步归约（E-Succ + E-IfFalse）得到 succ  true，没有类型，而且受阻了。
  • E-PredSucc 写成任意 𝑡，类型安全其实仍然成立，坏掉的是确定性，测试报出 pred ( succ ( pred 0 ) ) 有两种归约方式。

每条定理守住的东西不同，少证一条，就会漏掉一类错误。

1 [附注] 测试不是证明 [testing-is-not-proof]
  • 2026-10-10
  • Glomzzz

测试只能检查有限个样本，证明覆盖命题量词范围内的所有对象。例如， 用测试对照证明 的测试样本来自 [定义] 项的集合 的项集合，深度按 [定义] 大小与深度 计算；深度 3 的项已经多到没法穷举。测试过了，也只说明在这些样本上没找到反例。两者的分工是：证明负责“为什么对”，测试负责发现“证明和代码说的是不是同一件事”。测试失败，说明证明或代码有一处错了；证明写不下去，往往说明测试还没碰到反例。

这个差距在真实软件里大得惊人。MikanAffine 的《为什么 sqlite 可以被重写》以 SQLite 为例：它用约 9000 万行测试覆盖约 20 万行源码，仍然不断被报告出漏洞。原因是程序每经过一个 if if 就分裂出两条执行路径，要覆盖的路径数随分支数指数增长，测试的增长永远追不上。

类型系统走的是另一条路。 [推论] 类型安全 这样的定理不是对路径逐条检查，而是一次性地对所有良类型程序、所有执行路径断言“不会受阻”。前提是类型系统本身是可靠的（sound）：它说没问题的程序，运行时真的没有那一类问题。一个不可靠的类型系统（比如允许随意强制转换指针的 C）给出的“通过检查”就不能当作保证，该测的还得测。

这正是近年 RIIR（Rewrite It In Rust，用 Rust 重写）思潮背后最实在的理由。Rust 的类型系统和借用检查器把内存安全、数据竞争这类错误从“要靠测试和运气去发现”变成了“编译不通过”；RustBelt 等工作则在形式化层面证明了它的安全核心是可靠的。微软和 Chromium 都报告过，各自产品中约七成的严重安全漏洞来自内存安全问题；而 Android 在新代码转向内存安全语言之后，这类漏洞的占比显著下降。静态检查当然不能取代测试，但它把一整类错误从测试的负担里拿掉了，这是测试本身做不到的。

2 [注记] 证伪与证实 [falsification-and-verification]
  • 2026-10-10
  • Glomzzz

波普尔（Popper）认为，经验科学里的普遍命题无法被有限次观察证实，只能被一次反例证伪。测试的处境与此相同：一万个通过的样本不能证实“所有良类型程序都不受阻”，一个受阻的样本就能推翻它。

证明则走另一条路。它不观察，而是从定义出发推出结论，所以可以对无穷多个程序负责。代价是它只对定义负责：如果规则本身没有描述我们心里想的那门语言，证明再严密也帮不上忙。这说明了证明与测试的分工：证明管“从规则到结论”，测试和实现管“规则是不是我们想要的”。 [推论] 类型安全 与 用测试对照证明 分别给出了这两种工作的例子。

3 练习：测试与证明
本节练习（4题）

练习7.1：给不同的错误配不同的测试

分别对下面四处独立的错误设计一个具体输入与测试断言，并指出它违反了哪个性质：值 true 被归约成 0；pred 0 被误判为没有后继；关系中的 E-PredSucc 去掉数值限制；类型检查器不检查 else 分支。
提示分别检查值不可归约、进展、关系的所有后继，以及检查器接受后类型能否保持；测试一个函数只有一个返回值不是确定性测试。
参考答案
  • 让 step(True) step(True) 返回 Some(Zero) Some(Zero) ：用值不可归约测试要求 step(True) == None step(True) == None 。这个错误也把 Bool Bool 变成 Nat Nat ，所以保型检查也能发现。
  • 让 step(Pred(Zero)) step(Pred(Zero)) 返回 None None ：pred 0: Nat 不是值，却无法走一步，进展测试会失败。
  • 将关系中的 E-PredSucc 放宽到任意项：pred ( succ ( pred 0 ) ) 有两个不同后继 pred 0 与 pred ( succ 0 )。用独立的规则枚举器检查后继集合，而不是只看 step step 选出的一个返回值。
  • type_of type_of 忽略 else 分支：succ ( if  false  then 0 else  true ) 被错认为 Nat，一步得到 succ  true，新项没有类型且受阻。逐步保型或端到端安全测试能抓到它。

四处修改应分别注入、分别恢复，才能知道哪个测试在防哪类错误。放宽规则的错误不一定破坏类型安全，不能指望一条安全测试包办所有性质。

练习7.2：通过测试，还是没有真正测到？

本节的 safety safety 测试如果只生成不良类型项，或者只生成 true、false、0，会发生什么？怎样用统计断言发现这种空转？另解释为什么 assert_eq!(step(t), step(t)) assert_eq!(step(t), step(t)) ，或者从 step step 直接包装出的“关系枚举器”，不能验证求值器忠实于规则。
提示读 [附注] 测试不是证明 时也检查测试的前提：循环是否进入过良类型情形？是否实际走过一步？比较器是不是只在与自身比较？
参考答案

只生成不良类型的项时， let Some(ty) = type_of(&t) else { continue }; let Some(ty) = type_of(&t) else { continue }; 会跳过每个样本，进展和保型断言一次都不运行。只生成常量值时，类型检查会通过，但 step step 立即返回 None None ，仍从未检查一次类型保持。

至少统计并断言良类型样本数大于零、实际归约总步数大于零，再加入确实需要多步运行的嵌套项。还应单独测拒绝的项和受阻情形。这些统计能排除明显的空转，却不等于覆盖所有规则和路径。

assert_eq!(step(t), step(t)) assert_eq!(step(t), step(t)) 只是一个确定执行的函数与自身比较；即使它算错了，两边仍可能同时错。把“关系枚举器”直接写成 step(t).into_iter().collect() step(t).into_iter().collect() 也没有独立核对规则。应分别按规则列出后继，再与函数实现对照；两份代码仍可能犯相同错误，所以还需结合具体例子、逐规则审阅与证明。

练习7.3：再多的有限样本也留下边界

给定任意一批有限的测试项，设其中最大深度为 𝑑。构造一个检查器，使它通过这批项与正确 type_of type_of 的所有结果对照，却在某个更深的项上不可靠。给出函数、反例和推理，说明这个例子揭示的测试边界。
提示设这批样本的最大深度为 𝑑。让错误只在深度超过 𝑑 时出现。
参考答案

假设这批样本非空，𝑑 就是有限的最大深度；空样本集可取 𝑑=0。可以构造一个终止的错误检查器：

pub fn bounded_fake(t: &Term, d: usize) -> Option<Type> {
    if depth(t) > d { Some(Type::Nat) } else { type_of(t) }
}
pub fn bounded_fake(t: &Term, d: usize) -> Option<Type> {
    if depth(t) > d { Some(Type::Nat) } else { type_of(t) }
}

每个测试样本深度都不超过 𝑑，所以它们得到的结果与正确实现完全相同。可是给 true 外面包上 𝑑+1 层 succ，得到的项深度为 𝑑+1，会被假检查器接受为 Nat；原类型规则却无法给最内层 succ  true 定型，整个项没有类型，而且受阻。

因此有限测试通过，只能排除样本范围内已出现的反例。这里不声称真实 bug 一定这样写，而是用一个具体构造说明：没有关于所有项的证明，测试结果本身不蕴涵普遍可靠性。

练习7.4：为什么求值测试的循环会停？

不依赖类型安全，证明原语言每一步都使大小严格下降，并给出从大小为 𝑠 的项出发的归约步数上界。能否把大小换成深度并保持“每一步严格下降”？找反例。最后说明为何“循环停了”仍不足以断言求值成功。
提示对一步归约的推导归纳。计算规则删掉节点；同余规则把子项的严格下降带到外层。深度不一定严格下降。
参考答案

对 𝑡⟶𝑡 ′ 的推导归纳。E-IfTrue 与 E-IfFalse 只留下一个分支，删掉根、条件及另一分支，大小严格下降。E-PredZero 和 E-IsZeroZero 从两个节点变成一个；E-PredSucc 删除 pred 与 succ 两个节点；E-IsZeroSucc 把大小至少为 3 的项变成一个 false 节点。这覆盖六条计算规则。

对 E-Succ、E-Pred、E-IsZero， 归纳假设 给出子项大小严格下降，两边包上同一个一元节点，严格不等式仍成立。对 E-If，只有条件变化，两个分支与 if 根贡献的节点数相同，也保持严格下降。因此十条规则都给出 size( 𝑡 ′ )<size( 𝑡 )。∎

大小始终是至少为 1 的整数，起点大小为 𝑠 时，最多走 𝑠−1 步就必须停止。停止时是否为值是另一个问题：不良类型项也会停止，却可能受阻；对良类型项，进展才排除这种终点。

深度不适合替代这个严格下降度量。例如 if ( iszero 0 ) then ( succ ( succ 0 ) ) else 0 的第一步只把条件变成 true，最长路径仍在 then 分支，两项深度都是 3。类型安全也不独自保证循环停止，见本节之前的自循环扩展题。

References

[] 形式化入门：从 BNF 到类型安全 [index]

[定义] 归纳假设 [induction-hypothesis]

[附注] 分支顺序里藏着证明 [proofs-behind-pattern-matching-order]

[] 规则与算法：可靠性与完备性 [rules-and-algorithms]

[] 回头看与延伸阅读 [summary]

Backlinks

[附注] 为什么 E-PredSucc 要求 [numeric-value-restriction-in-predecessor-reduction]

[] 规则与算法：可靠性与完备性 [rules-and-algorithms]

[] 回头看与延伸阅读 [summary]

Based on Typsite