. 用测试对照证明

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!(size(&next) < size(&cur), "{cur:?} ⟶ {next:?}");
            // 保型：一步规约，类型不变
            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!(size(&next) < size(&cur), "{cur:?} ⟶ {next:?}");
            // 保型：一步规约，类型不变
            assert_eq!(type_of(&next), Some(ty), "{cur:?} ⟶ {next:?}");
            cur = next;
        }
    }
}

规约使大小严格下降证明的是原求值关系的每一步都让项变小，测试却不能预先假定待测 step step 已正确实现这个关系．因此这里也检查 size size 严格下降：若错误实现返回原项，测试会立刻报错，避免陷入死循环．它防范的是“每次调用都会返回，但后继不下降”的错误；若 step step 自己不返回或耗尽资源，仍需测试进程的超时或其他限制，见算术语言形式化的未展开前提．

完整工程在 code/plt-arith code/plt-arith 下；进入该目录运行 cargo test --release cargo test --release ．实际测试还保留 size(t) size(t) 次调用的上限，并明确确认求值器曾返回 None None ，不能仅凭当前项是值就认定已经停止；同时统计良类型样本与实际规约步数，防止测试空转．样本是深度 2 以内的全部 59439 个项，外加 50000 个深度到 6 的确定性随机项．

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

前文提过的两个错误写法都会暴露出来，但抓住它们的测试不同．当 type_of type_of 不检查 $else$ 分支时，破坏的是检查器相对原类型规则的可靠性（原规则的保型定理仍成立，失效的是“检查器接受的项都满足规则”）： safety safety 实际报出的反例是 $succ (if false then 0 else true)$ ，错误的检查器只看 $then$ 分支，认为它是 $Nat$ ，一步规约（E-Succ + E-IfFalse）后得到 $succ true$ ，没有类型且受阻，测试通过“规约后类型不再保持”暴露了这个检查器错误．而当 E-PredSucc 放宽为任意 $𝑡$ 时，类型安全其实仍然成立，坏掉的是确定性，确定性测试会报出 $pred (succ (pred 0))$ 有两种规约方式．

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

Note 1 测试与证明的边界 [testing-is-not-proof]

2026-10-10
Glomzzz

打开独立页面 →

Remark 2 证伪与证实 [falsification-and-verification]

2026-10-10
Glomzzz

打开独立页面 →

3 练习：测试与证明

Exercises (4)

Exercise 7.1. 给不同的错误配不同的测试

分别对下面四处独立的错误设计具体输入与测试断言，并指出它违反了哪个性质：值

true

规约成

0

；

pred 0

误判为没有后继；关系中的 E-PredSucc 去掉数值限制；类型检查器不检查

else

分支．

Hint

分别检查值不可规约、进展、关系的所有后继，以及检查器接受后类型能否保持；单看一个函数返回单个结果，测不出关系本身的确定性．

Solution

若让 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$ ，逐步保型或端到端安全测试能抓到它．

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

Exercise 7.2. 测试空转与自比较

分析本节的 safety safety 测试在只生成不良类型项，或者只生成

true

、

false

、

0

时会发生什么，说明怎样用统计断言发现这种空转；另说明 assert_eq!(step(t), step(t)) assert_eq!(step(t), step(t)) 以及从 step step 直接包装出的“关系枚举器”为何无法验证求值器与规则一致．

Hint

读测试与证明的边界时也检查测试的前提：核对循环是否进入过良类型情形、是否实际走过一步，以及比较器是否仅在与自身比较．

Solution

只生成不良类型的项时， 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() 也没有独立核对规则．应分别按规则列出后继，再与函数实现对照；两份代码仍可能犯相同错误，所以还需结合具体例子、逐规则审阅与证明．

Exercise 7.3. 再多的有限样本也留下边界

给定任意一批有限的测试项，设其中最大深度为

𝑑

．构造一个检查器，使它通过这批项与正确 type_of type_of 的所有结果对照，却在某个更深的项上不可靠．给出函数、反例和推理，说明这个例子揭示的测试边界．

Hint

设这批样本的最大深度为

𝑑

．让错误只在深度超过

𝑑

时出现．

Solution

假设这批样本非空， $𝑑$ 就是有限的最大深度；空样本集可取 $𝑑 = 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$ 定型，整个项没有类型，而且受阻．

因此有限测试通过，只能排除样本范围内已出现的反例．这个构造无需模拟真实缺陷的常见写法，就足以表明：没有关于所有项的证明，测试结果本身不蕴涵普遍可靠性．

Exercise 7.4. 求值测试循环的终止性

不依赖类型安全，证明原语言每一步都使大小严格下降，并给出从大小为

𝑠

的项出发的规约步数上界．判断能否把大小换成深度并保持“每一步严格下降”（若不能则给出反例），最后说明为何“循环停了”仍不足以断言求值成功．

Hint

对一步规约作规则归纳．基本规约规则删掉节点；结构规则把子项的严格下降带到外层．深度不一定严格下降．

Solution

对 $𝑡 ⟶ 𝑡^{'}$ 作规则归纳． 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

Backlinks