上手 AlphaProof Code：为关键 Python 函数写规约并验证

这篇能做出什么

照着做完，你会得到三样具体的东西：

1. 一个带形式化规约的 Python 小模块，规约本身就是可执行的断言，不是注释。

2. 一次完整的“验证失败 → 读反例 → 补前置条件 → 验证通过”闭环。你会亲眼看到验证器给出 lo=5, hi=1, x=3 这种具体输入，而不是一句“测试没覆盖到”。

3. 一套把验证接进 CI 的配置，让规约和单元测试一起跑。

先明确一件事：形式化验证不是单元测试的升级版，两者检查的是不同维度。

所以真实的用法是：用形式化规约锁住关键函数的契约，用单元测试锁住业务行为，两者不互相替代。

前置条件清单

动手前把下面这些备齐，能省掉大半卡壳时间。

• Python 环境：一个较新的 Python 3.x，用虚拟环境隔离。AlphaProof Code 支持的最低版本以官方文档为准。
• AlphaProof Code 本身：获取方式、许可证、CLI 子命令名以官方页面和 --help 输出为准。本文里的命令形态用于说明工作流，你实际执行前先跑一次 --help 确认参数拼写。
• 一个 SMT 求解器：多数这类工具内部会调用 Z3 一类的求解器。本文的示例用 z3-solver，可以直接 pip 装。
• 契约库：deal，用来把规约写成随函数一起跑的形式，这样即使不接验证器，规约也能在测试里生效。
• 属性测试库：hypothesis，用来做对照实验。
• Git：验证失败要能回滚，规约改动要能 review。
• 一点命题逻辑常识：知道“蕴含”“全称量词”是什么意思就够起步了。

安装一条命令解决后面三个：

```bash

python -m venv .venv

source .venv/bin/activate # Windows 用 .venv\Scripts\activate

pip install deal hypothesis z3-solver crosshair-tool

```

第 0 步：先搞清楚“规约”在写什么

规约（specification）就是把函数的“口头承诺”写成逻辑公式。分三块：

• 前置条件（precondition）：调用方必须保证的事。你违反了，函数不负责。
• 后置条件（postcondition）：函数必须保证的事。只要前置成立，返回时后置一定成立。
• 不变量（invariant）：循环或对象状态在每一步都成立的性质。

用一句话概括 clamp(x, lo, hi) 的契约：

> 只要 lo <= hi，返回值一定落在 [lo, hi] 区间内，并且要么等于 x，要么等于边界值。

把这句话翻译成逻辑：

```

pre: lo <= hi

post: lo <= result <= hi ∧ (result == x ∨ result == lo ∨ result == hi)

```

这就是全部。剩下的工作是把它交给工具去证。

第 1 步：准备一个有坑的函数

新建 src/mathkit/clamp.py：

```python

def clamp(x: int, lo: int, hi: int) -> int:

if x < lo:

return lo

if x > hi:

return hi

return x

```

再配三个“看起来够了”的单元测试：

```python

def test_below():

assert clamp(-5, 0, 10) == 0

def test_above():

assert clamp(42, 0, 10) == 10

def test_inside():

assert clamp(7, 0, 10) == 7

```

三个全绿。但这三个测试永远发现不了一件事：当 lo > hi 时，这个函数的行为是什么？clamp(3, 5, 1) 会返回 5，而 5 > hi。这不是 bug，是契约没写清楚——函数从没承诺过 lo > hi 时该怎么办，但调用方也不知道自己踩进了未定义区。

第 2 步：手写第一版规约

不要一上来就让工具生成。先自己写一遍，你才知道工具生成的版本哪里不对。

用 deal 把规约写成可执行的：

```python

import deal

@deal.pre(lambda x, lo, hi: lo <= hi)

@deal.ensure(lambda x, lo, hi, result: lo <= result <= hi)

@deal.ensure(lambda x, lo, hi, result: result in (x, lo, hi))

@deal.pure

def clamp(x: int, lo: int, hi: int) -> int:

if x < lo:

return lo

if x > hi:

return hi

return x

```

几个要点：

• @deal.pre 的 lambda 参数是函数的入参名，不是位置参数。写错名字会静默失效。
• @deal.ensure 的 lambda 多一个 result，代表返回值。
• @deal.pure 声明这是纯函数（无副作用），验证器拿到这个信息可以做得更多。
• 装饰器从下往上生效，@deal.pure 在最下面。

此时跑一遍 pytest，规约会在运行时被检查。但注意：运行时检查只能发现你真的调用到的输入，本质上还是测试。要覆盖全部输入，得靠验证器。

第 3 步：让 AlphaProof Code 生成规约草案

这一步的流程通常是：把工具指向目标文件或函数 → 它读取类型注解、docstring、函数体 → 吐出一份规约草案（前置条件、后置条件，有时还有循环不变量）→ 你来审。

命令形态大致如下（子命令名以官方文档为准）：

```bash

alphaproof spec src/mathkit/clamp.py --function clamp

```

工具大概率会给你一份正确但没什么用的规约，比如后置条件只写了 isinstance(result, int)。这很正常：生成器倾向于写“一定能证出来”的弱规约。

审阅时用这个标准卡一遍：

> 规约里的每一条，要么描述了业务约束，要么描述了你真正担心出错的点。做不到这两点的，删掉。

isinstance(result, int) 这种由类型注解已经保证的东西，写进规约只会让证明负担变重、信息量变零。

第 4 步：跑验证，读懂反例

先故意跑一个不加前置条件的版本，看看会发生什么：

```bash

alphaproof verify src/mathkit/clamp.py --function clamp

```

输出示意：

```

[FAIL] clamp

counterexample: x=3, lo=5, hi=1

violated: postcondition #1 (lo <= result <= hi)

result = 5

```

这三行信息量很大：

• counterexample 是一组具体的、必然违反规约的输入。不是随机采样，是求解器构造出来的。
• violated 告诉你哪一条后置条件挂了。
• result = 5 是这组输入下的返回值。

反例怎么解？代进去验算：x=3, lo=5, hi=1，3 < 5 成立，所以走第一个分支返回 lo = 5。然后检查 lo <= result <= hi，即 5 <= 5 <= 1，5 <= 1 为假。反例成立。

这就是形式化验证和单元测试的根本差别：它不会说“我没测到”，它直接给你一个能复现的输入。

想更直观地理解背后的机制，可以用几行 Z3 把同一件事跑一遍：

```python

from z3 import Ints, Solver, And, Not, If

x, lo, hi, r = Ints("x lo hi r")

s = Solver()

s.add(lo <= hi) # 前置条件

s.add(r == If(x < lo, lo, If(x > hi, hi, x))) # 函数体语义

s.add(Not(And(lo <= r, r <= hi))) # 后置条件的否定

print(s.check()) # unsat 表示后置条件必然成立

```

把 s.add(lo <= hi) 那一行注释掉再跑，s.check() 会返回 sat，并给出一个模型——那就是反例。

第 5 步：补前置条件，再验证

把 lo <= hi 写进规约，重跑验证。这次应该通过。

但这里有个必须讲清楚的分歧：加前置条件到底是在修 bug，还是在推卸责任？

判断方法很简单——看真实调用方：

• 如果调用方必然满足 lo <= hi（比如 lo、hi 来自同一个已验证的配置对象），那前置条件是在陈述事实，加进去是对的。
• 如果调用方可能传 lo > hi（比如用户输入、外部接口），那加前置条件就是把 bug 藏起来了。

后一种情况，正确的做法是让函数自己处理：

```python

import deal

@deal.raises(ValueError)

@deal.ensure(lambda x, lo, hi, result: lo <= result <= hi)

@deal.pure

def clamp(x: int, lo: int, hi: int) -> int:

if lo > hi:

raise ValueError("lo must be <= hi")

if x < lo:

return lo

if x > hi:

return hi

return x

```

前置条件消失了，代价是引入了一个可能抛出的异常。规约里的 @deal.raises 就是在告诉验证器“这条路径是合法的”。

契约的每一次放松，都要在代码里显式付出代价。 这是写规约最有价值的副产品：它逼你想清楚边界情况归谁管。

第 6 步：换一个需要真证明的函数

clamp 太简单了，分分钟证完。换一个需要点推理的。新建 src/mathkit/split.py：

```python

import deal

@deal.pre(lambda total, parts: parts >= 1)

@deal.ensure(lambda total, parts, result: len(result) == parts)

@deal.ensure(lambda total, parts, result: sum(result) == total)

@deal.ensure(lambda total, parts, result: max(result) - min(result) <= 1)

@deal.pure

def split_evenly(total: int, parts: int) -> list[int]:

"""把 total 尽量均匀地切成 parts 份。"""

base, rem = divmod(total, parts)

return [base + 1] * rem + [base] * (parts - rem)

```

三条后置条件分别说：份数对、总和守恒、任意两份相差不超过 1。这三条合起来，就完整刻画了“均匀切分”这个语义——比 assert split_evenly(10, 3) == [4, 3, 3] 强得多，因为它覆盖了负数、parts=1、total 极大等所有情况。

前置条件 parts >= 1 是必须的：parts = 0 会直接 ZeroDivisionError。注意这是 Python 的 divmod 在负数上向下取整，所以 total 为负时规约依然成立——这一点值得你手动验算一遍，divmod(-7, 3) 得到 (-3, 2)，结果 [-2, -2, -3]，和为 -7，极差为 1。

跑验证：

```bash

alphaproof verify src/mathkit/split.py --function split_evenly

```

如果一次通过，恭喜。如果没有，往下看第 7 步。

顺手加一个属性测试做对照：

```python

from hypothesis import given, strategies as st

@given(st.integers(-106, 106), st.integers(1, 50))

def test_split_properties(total, parts):

out = split_evenly(total, parts)

assert len(out) == parts

assert sum(out) == total

assert max(out) - min(out) <= 1

```

属性测试跑几千组随机输入，形式化验证覆盖全部输入。前者帮你发现规约写错了，后者帮你保证规约没漏。

第 7 步：证明卡住时怎么办

验证器不是万能的。它在两类问题上容易卡住：量词（“存在某个下标 i 使得……”）和非线性算术（乘法、除法混在一起）。遇到超时或 unknown，按下面的顺序处理。

情况一：规约根本写不出来

比如你想验证一个去重函数，要求“结果保持原顺序”：

```python

def dedupe_sorted(xs: list[int]) -> list[int]:

if not xs:

return []

out = [xs[0]]

for v in xs[1:]:

if v != out[-1]:

out.append(v)

return out

```

“保持原顺序”没法用一句 sum(result) == ... 表达，它是个存在性命题。做法是抽一个纯辅助函数，把它当作规约里的定义使用：

```python

def is_subsequence(sub: list[int], xs: list[int]) -> bool:

it = iter(xs)

return all(any(v == w for w in it) for v in sub)

```

然后在规约里写 @deal.ensure(lambda xs, result: is_subsequence(result, xs))。

注意：辅助函数本身也得是“一眼可读、语义明确”的，否则你只是把证明义务转移到了一个没人看得懂的判断里。

情况二：证得出来但太慢

给验证器“指路”——把一个大证明拆成几个中间断言。比如循环不变量，不要指望工具一次猜中，直接写成多条独立的 ensure，每一条都断言一个局部性质。工具证 N 个小命题，比证一个大命题快得多。

情况三：规约太强，超过了实际需要

形式化验证的目标不是“证出最强的性质”，是“证出够用的性质”。如果一条后置条件证不出来、但又确实不是业务关心的，删掉它比死磕划算。

第 8 步：接进 CI

规约和测试一样，不跑就会腐坏。加到 .github/workflows/verify.yml：

```yaml

name: verify

on: [push, pull_request]

jobs:

contracts:

runs-on: ubuntu-latest

steps:

• uses: actions/checkout@v4
• uses: actions/setup-python@v5

with:

python-version: "3.x"

• name: Install

run: |

python -m pip install --upgrade pip

pip install -r requirements-dev.txt

• name: Runtime contracts

run: pytest -q

• name: Symbolic check

run: crosshair check src/mathkit/clamp.py src/mathkit/split.py

• name: Formal verification

run: alphaproof verify src/mathkit/ --timeout 60

```

几点说明：

• crosshair-tool 是另一条独立的检查路径，用符号执行找反例，和 SMT 求解互补。两个都挂说明规约真有问题，只有一个挂说明是工具能力边界。
• 验证步骤一定要设 --timeout（具体参数名以官方文档为准），否则一次 unknown 能把 CI 挂满一小时。
• 把验证放在独立的 job 里，别和单元测试混在一起。单元测试红了要立刻修，验证红了可以先降级成告警——规约的修复往往需要设计层面的讨论。

常见坑与排错

反例里的变量名和函数参数对不上。 通常是 lambda 里写了位置参数或者拼错了名字。@deal.pre 的 lambda 参数必须和函数签名一致，否则条件恒为真、静默失效。

规约里调用了被测函数自己。 这是循环论证，工具会当成公理接受，证出来的是“若 P 则 P”。规约里只能调用更基础的、已被独立验证的纯函数。

整数除法的语义陷阱。 Python 的 // 和 % 对负数是向下取整，而一些 SMT 后端默认向零取整。同一份规约在两边含义不同，会导致“证过了但跑起来不对”。涉及负数除法时，显式写出取整方向，或者干脆把输入限定为非负。

浮点数不要直接进规约。 SMT 里的实数类型是数学意义上的实数，和 IEEE 754 的双精度不是一回事。涉及金额、比例的地方，先换成整数（以分为单位）再验证。

空列表和 None。 max([])、sum([])、len(None) 在 Python 里行为各不相同，规约里只要出现 max(result)、min(result)，就必须显式加上 len(result) >= 1 的前置条件，否则函数自己会先崩。

把工具生成的规约直接提交。 生成器不知道你的业务语义，它只保证“看起来能证”。没有人工 review 的规约，等于给自己发了一张假的合格证。

把要证的东西假设进去了。 有些工具支持 assume / axiom，用来声明“这条当公理”。用之前先问自己：这条真的不需要证吗？把关键性质写成公理，是最隐蔽的自欺。

验证通过 ≠ 完全正确。 验证保证的是“后置条件在前置条件成立时必然成立”。前置条件写松了、后置条件写弱了，验证照样通过，但函数照样可能错。规约的质量永远取决于写规约的人。

下一步建议

从这三类函数开始选。 钱（金额计算、分摊、汇率换算）、权限（谁能访问什么）、边界（分页、切片、超时计算）。它们的共同点是有明确的业务不变量，规约写出来别人看得懂，出错代价又高。

先只验证关键路径，不要全项目铺开。 一个模块里挑 3 到 5 个函数，把规约写扎实、接进 CI、跑上两周，再决定要不要扩大范围。一上来全量铺开，规约的质量一定崩。

建立规约评审习惯。 规约的改动和代码改动一样走 PR，让第二个人读一遍“这条后置条件是不是真的业务要求”。规约的 bug 比代码的 bug 更难发现，因为它是“证明对了但证错了东西”。

补一点证明助手的基础。 用熟这类工具之后，去读一点 Lean 或 Dafny 的入门材料，你会更容易理解验证器为什么在某些地方卡住、中间断言该怎么加。

度量口径换成“已验证的关键函数数”。 不要统计规约行数或者验证覆盖率——那种数字涨得很快，说明不了任何问题。真正有意义的是：线上曾经出过事故的那几个函数，现在有没有规约。