Why3 — 写一次程序规范，多个证明器一起来证

待复核

是什么

Why3 是一个程序验证平台：你用它的语言 WhyML 写代码 + 写”代码应该满足什么”，平台自动把这些条件翻译成数学题，同时丢给好几个证明器（Z3、Alt-Ergo、CVC4、Coq…）去解。

日常类比：像考试时把同一道难题复印多份发给一屋子专家——有人擅长代数、有人擅长几何。谁先解出来，你就接受谁的答案；都解不出，再自己人工补刀。

你写：

let factorial (n: int) : int
  requires { n >= 0 }
  ensures  { result >= 1 }
= ...

requires / ensures 就是你给函数的”出题”。Why3 自动生成”如果 n >= 0，那么 result >= 1”这道证明题，然后分发出去。

为什么重要

不理解 Why3，下面这些事都不好理解：

为什么 SPARK / Frama-C Jessie / CryptoLine 这些验证 C / Ada 代码的工具，常以 Why3 为验证后端
为什么”证明器多样化”是工程必需——同一道题 Z3 卡 30 秒、Alt-Ergo 0.1 秒，反过来也常见
为什么 F*、Dafny、Viper 这些后辈的设计都绕不开”VC 生成 + 多后端”这条路
为什么 2013 年的工具到 2026 年还在更新——它解的是”中间表示”问题，跟具体证明器解耦

核心要点

Why3 的设计可拆成三层：

前端（WhyML）：带契约的 ML 风格语言。支持纯函数、异常、可变引用、循环不变量。还可以写 ghost code——只为了证明而存在，编译生成可执行代码时会被擦掉。
中间层（VC 生成器）：基于 Hoare 逻辑里的 weakest precondition 演算（hoare-logic）。把”程序 + 契约”翻译成一堆纯逻辑公式，叫 verification conditions（VC）。
后端（driver）：每个证明器（Z3 / Alt-Ergo / CVC4 / Coq / Isabelle）配一个驱动文件，声明：这个证明器支持哪些理论、关键字怎么翻译、不支持的算子怎么编码。同一组 VC 可以同时打给 N 个后端。

平台不发明新理论，它发明的是”解耦”——程序员、证明义务、证明器三者各干各的。

类比：Why3 之于程序验证，相当于 LLVM 之于编译——前者把”程序+规范”折成一种通用 IR 喂给一群求解器，后者把源语言折成 LLVM IR 喂给一群目标后端。两边都是靠中间表示分摊生态。

实践案例

案例 1：写一道带循环不变量的题

let sum_to (n: int) : int
  requires { n >= 0 }
  ensures  { result = n * (n + 1) / 2 }
= let ref s = 0 in
  for i = 1 to n do
    invariant { s = i * (i - 1) / 2 }
    s <- s + i
  done;
  s

逐部分解释：

requires / ensures：入口保证 n >= 0，出口保证结果是等差求和公式
let ref s = 0：可变累加器；循环里用 s <- s + i 更新
invariant：Why3 强制你写”每轮都成立的事实”；它会生成三道子题——进入时成立、循环体保持、退出后推出 ensures——再分发给各后端

案例 2：自动器卡住，人工 Coq 接力

某些 VC 涉及复杂归纳（比如树高度不等式），SMT（z3-2008）会超时。IDE 里可以这样接力：

看哪一道 VC 红灯超时（其余绿灯可先不管）
右键该题 → “切到 Coq”；Why3 生成类似下面的脚手架：

Lemma tree_height : forall t, height t >= 0.
Proof.
  intros t. induction t.
  - (* 叶子：自动器常能收 *) admit.
  - (* 节点：你手写归纳步 *) simpl; lia.
Qed.

你只补归纳那一步；证完后 IDE 把这道题标绿

这种”自动 90% + 人工 10%“是 Why3 能落地的关键：边界可移动，不必整文件改写证明器。

案例 3：CryptoLine 借 Why3 证密码代码

CryptoLine 把椭圆曲线乘法这类位级 C 代码译成 WhyML（下面是教学伪代码）：

let mul_mod (a b m: int) : int
  requires { m > 0 /\ 0 <= a < m /\ 0 <= b < m }
  ensures  { result = (a * b) mod m }
= let ref r = 0 in
  (* 由 C 的移位/加法展开而来 *)
  for i = 0 to 31 do
    if (b / (2 ^ i)) % 2 = 1 then r <- (r + a) % m
  done; r

逐部分解释：

前端只认 WhyML 契约，不直接读 C
VC 生成器把”实现 ≡ 数学 mod”拆成一堆公式
Z3 啃位向量约束，Coq 啃代数性质——同一组 VC，多后端分工

需要”证明用变量”时写 ghost（编译擦掉、运行时零开销）；细节见核心要点里的 ghost code。

踩过的坑

VC 数量爆炸：一个看似简单的函数，因为分支多、循环多、契约多，可能生成几百道 VC。需要靠后端缓存 + 并行 + 选择性触发证明来扛。
WhyML 不是”通用语言”：它没设计成给人写产品代码用的。要验证 C / Ada / Rust，得先翻译进 WhyML，翻译器（Jessie、SPARK、Creusot）本身就是大工程。
驱动文件写错全盘崩：把 mod 翻译成 Z3 的 bvurem 还是 mod，参数顺序错了，证明器返回 “unsat” 但其实题目本身被歪曲了。Why3 团队为此积累了上千行的标准 driver 库。
自动器之间不互通：Z3 解出来 Alt-Ergo 不一定信。Why3 不复用证明结果，每个后端各跑各的——好处是简单，代价是浪费算力。
别名（alias）很难处理：可变引用一旦指向同一块内存，VC 推导会爆炸。Why3 用类型不变量 + region 推断避免别名进入逻辑层；代价是 WhyML 写起来比通用 ML 多几条限制。

适用 vs 不适用场景

适用：

验证已有命令式代码（C / Ada / Rust）→ 经 Frama-C Jessie / SPARK / Creusot 接到 Why3
密码原语、内核模块、几百行关键算法的功能正确性（典型：单文件 / 单模块规模）
想要”自动证明优先 + 人工证明兜底”的混合工作流

不适用：

验证机器学习模型（值域是浮点 + 概率，不是离散逻辑）
验证 UI / 网络协议交互（时序验证，更适合 lamport-tla-1994）
整仓业务应用——注解与 VC 成本远高于收益；WhyML 也不是产品语言

历史小故事（可跳过）

1990 年代：Filliâtre 在巴黎南大博士期间做 Why（v1），原型只接 Coq 后端
2003 年：Why2 加入多后端支持，Frama-C / Jessie 开始用
2010 年：Filliâtre + Paskevich 重写为 Why3，前端从 ML 子集改造成完整 WhyML
2013 年：ESOP 论文正式介绍 Why3 平台，成为欧洲程序验证的事实标准
同代竞品 Boogie（boogie-2005，Microsoft）走类似思路但更轻量；F*（fstar）则把 Why3 思路 + 依赖类型揉到一门语言里

学到什么

解耦比创新更工程化：Why3 没发明新证明算法，它发明了”前端 / VC / 后端”的分层，让生态可以独立演化
多后端不是冗余而是必需：不同求解器擅长不同理论，工程上赌单一后端会很疼
自动 + 人工的边界要可移动：靠 driver + IDE 让程序员能在任意一道 VC 上”降级”到人工证明
中间语言比通用语言重要：WhyML 自己不流行，但它常作为 Frama-C Jessie / SPARK / CryptoLine 的验证后端翻译目标

关联

hoare-logic —— Why3 把 Hoare 三元组系统化成 VC 生成器
boogie-2005 —— Microsoft 同代竞品；Boogie 偏轻量、Why3 偏完整
z3-2008 —— SMT 求解器，Why3 默认后端之一
isabelle-hol-2002 —— 当自动器卡住时的人工后端选项
fstar —— Why3 思路的现代继承者

反向链接

boogie-2005 —— Boogie — 写一次验证后端，多种证明语言复用
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
vcc-2009 —— VCC — 给并发 C 加注解，让 SMT 自动证它对