3.3 程序正确性：规格、循环不变量与终止性
一段代码通过了现有测试，塔里的证明师仍追问：测试没覆盖的输入，凭什么相信它也满足规格？
“这个函数通过了所有测试”与“这个函数满足规格”不是同一句话。测试、静态分析、模型检查和证明提供不同范围的证据；程序正确性首先要求我们说清楚要证明哪个性质。
从前置条件和后置条件开始
Hoare 三元组写作：
{P} C {Q}P：执行命令C前必须成立的前置条件；C：程序或语句；Q：若执行按要求结束，之后必须成立的后置条件。
例如：
{amount > 0 ∧ balance ≥ amount}
balance := balance - amount
{balance ≥ 0}三元组没有自动说明调用者一定提供合法 amount，也没有说明程序一定终止。规格的责任要分开：调用者建立前置条件，被调程序保证后置条件。
部分正确与全正确
部分正确性：若程序终止，则结果满足后置条件。
全正确性：程序终止，并且结果满足后置条件。
int zero() {
while (true) { }
}“若该函数返回，则返回 0”在逻辑上可能作为部分正确性陈述成立，因为它从不返回；但它显然不满足“函数最终返回 0”的全正确性。
生产规格还可能包括时间、内存、并发和容错性质。数学上的功能正确，不等于系统在资源约束下可用。
赋值会改变状态
要保证执行：
x := x + 1之后 x>0，执行前应满足什么？把后置条件中的新 x 替换成赋值表达式：
x+1 > 0
⇔ x > -1这是一种向后推导前置条件的思路。多条语句可从最终目标逐步向前计算，但分支、循环和异常会产生更多证明义务。
分支必须覆盖两条路径
int abs(int x) {
if (x >= 0) return x;
return -x;
}想证明返回值非负，需要分别考虑：
x≥0路径返回x；x<0路径返回-x。
还要注意机器整数溢出：在 Java 中 -Integer.MIN_VALUE 仍是负数。若规格声称对全部 int 返回非负，源码实际上不满足。可以缩小前置条件、改用更宽类型，或明确溢出处理。
数学整数与机器整数的差异必须进入模型。
循环不变量连接每次迭代
考虑求数组前缀和：
long sum(int[] values) {
long total = 0;
int i = 0;
while (i < values.length) {
total += values[i];
i++;
}
return total;
}一个循环不变量是：
0 ≤ i ≤ values.length
total = values[0] + ... + values[i-1]证明分三步：
- 初始化：循环前
i=0,total=0，空前缀之和为 0； - 保持：若迭代前不变量成立且
i<n，加入values[i]并令i增一后，不变量仍成立； - 退出：退出条件给出
i≥n，与不变量的i≤n合并得i=n，所以total是整个数组之和。
不变量不是循环结束后才成立的目标，而是在每次检查循环条件时都成立的桥梁。
终止需要下降量
证明循环终止，常找一个变体（ranking function）：
- 取值在良基集合中，常用非负整数；
- 每次迭代严格下降；
- 不可能无限下降。
上例可用：
values.length - i循环体每次使 i 增 1，因此变体减 1；守卫 i<n 保证进入循环时变体为正。
并非所有终止证明都能用一个简单整数。递归、图遍历和并发协议可能需要词典序度量、多重集序或公平性假设。
二分查找里的不变量
对升序数组查找目标，可维护半开区间 [low, high)：
0 ≤ low ≤ high ≤ n
若 target 存在，则它只可能位于 [low, high)每次选择 mid 后：
- 若
a[mid] < target，令low=mid+1； - 若
a[mid] > target，令high=mid； - 否则返回
mid。
区间长度 high-low 严格下降，因此终止。退出时 low=high，候选区间为空，可推出目标不存在。
采用半开区间不是唯一正确方案，但下标定义、守卫和更新必须属于同一套不变量。混用闭区间和半开区间，是二分查找越界或死循环的常见来源。
测试与证明提供不同证据
“测试只能发现 bug，不能证明没有 bug”是过度概括。若输入域有限且测试穷尽全部状态，测试可以证明该模型范围内的性质；模型检查也能穷尽有限状态空间。问题在于真实系统的输入、时间和并发状态通常太大，测试覆盖只是其中一部分。
| 方法 | 强项 | 边界 |
|---|---|---|
| 单元/示例测试 | 具体行为、回归 | 覆盖有限 |
| 属性测试 | 大量生成输入、缩小反例 | 仍非一般穷尽 |
| 模糊测试 | 非预期输入和解析器缺陷 | 难表达完整功能规格 |
| 静态分析 | 无需运行覆盖多路径 | 抽象可能误报或漏报 |
| 模型检查 | 穷尽有限模型状态 | 状态爆炸、模型偏差 |
| 演绎证明 | 对规格建立通用保证 | 规格、工具和可信基也可能有错 |
可靠工程通常组合多种证据。证明核心算法不替代集成测试；测试外部依赖也不替代不变量推理。
规格错了，证明也会忠实地证明错事
证明工具只能判断实现是否满足给定模型。若规格漏掉“不能修改其他账户”，一个转账函数即使清空所有账户后设置目标余额，也可能满足过弱的局部后置条件。
规格评审应检查：
- 正常结果；
- 错误和异常；
- 未改变的状态；
- 边界与溢出；
- 终止和资源限制；
- 并发环境假设。
形式化的最大收益往往出现在写规格时：模糊需求被迫变成可讨论的条件。
完成检查
为“返回数组最大值”的函数完成：
- 写出空数组的处理方式和前置条件；
- 写出后置条件：结果属于数组，且不小于每个元素；
- 给出扫描循环的不变量；
- 给出终止变体；
- 说明整数类型、并发修改和异常是否在模型中；
- 设计示例测试、属性测试和一种静态或形式化检查。