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这是一种向后推导前置条件的思路。多条语句可从最终目标按执行顺序的逆序追溯，但分支、循环和异常会产生更多证明义务。
这里使用无溢出的数学整数。若 x 是 Java int，x=Integer.MAX_VALUE 使 x+1 溢出，虽满足 x>-1 却不满足后置条件。对这条机器语句，需要 0≤x<Integer.MAX_VALUE 才保证结果为正。
分支必须覆盖两条路径
int abs(int x) {
if (x >= 0) return x;
return -x;
}想证明返回值非负，需要分别考虑：
x≥0路径返回x；x<0路径返回-x。
还要注意机器整数溢出：在 Java 中 -Integer.MIN_VALUE 仍是负数。若规格声称对全部 int 返回非负，源码实际上不满足。可以缩小前置条件、改用更宽类型，或明确溢出处理。
数学整数与机器整数的差异必须进入模型。
若返回类型允许为 long，可在负数分支使用 return -(long) x;，先拓宽再取负，最小 int 会得到 2147483648L。写成 (long) (-x) 则太晚，取负时已经在 int 中溢出。
循环不变量连接每次迭代
考虑求数组前缀和：
前置条件为 values != null，并且执行期间数组内容不被其他线程修改；后置条件是返回入口快照中全部 int 元素的数学总和。下面是放在 Java 类中的方法：
long sum(int[] values) {
long total = 0;
int i = 0;
while (i < values.length) {
total += values[i];
i++;
}
return total;
}令 n=values.length，一个循环不变量是：
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是整个数组之和。
不变量不是循环结束后才成立的目标，而是在每次检查循环条件时都成立的桥梁。
还要验证 long 不溢出。Java 数组长度至多 2³¹−1，每个 int 的绝对值至多 2³¹，任意前缀和的绝对值因此小于 2⁶²，落在 long 范围内。这个结论依赖元素类型与数组长度；把参数改成 long[] 后不能照搬。类型范围与 length 类型见 JLS 21 的整数类型和数组成员。
终止需要下降量
证明循环终止，常找一个变体（ranking function）：
- 取值在良基集合中，常用非负整数；
- 每次迭代严格下降；
- 不可能无限下降。
上例可用：
values.length - i循环体每次使 i 增 1，因此变体减 1；守卫 i<n 保证进入循环时变体为正。
并非所有终止证明都能用一个简单整数。递归、图遍历和并发协议可能需要词典序度量、多重集序或公平性假设。
下降量必须结合循环体自身终止和执行环境来判断；一个等待网络响应的循环体，不能仅凭外层计数器下降就证明总会返回。Dafny 的 Termination 教程 给出了 decreases 度量的具体规则。
二分查找里的不变量
对升序数组查找目标，可维护半开区间 [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，候选区间为空，可推出目标不存在。
采用半开区间不是唯一正确方案，但下标定义、守卫和更新必须属于同一套不变量。混用闭区间和半开区间，是二分查找越界或死循环的常见来源。
下面的完整 Python 3 示例要求 values 是不被并发修改的非降序整数列表；有重复值时允许返回任一匹配下标：
def binary_search(values, target):
low, high = 0, len(values)
while low < high:
mid = low + (high - low) // 2
if values[mid] < target:
low = mid + 1
elif values[mid] > target:
high = mid
else:
return mid
return -1
print(binary_search([], 3)) # -1
print(binary_search([1, 2], 1)) # 0
print(binary_search([1, 2, 2, 4], 2)) # 2: any matching index is allowed.
print(binary_search([1, 2], 3)) # -1mid=low+(high-low)//2 落在非空候选区间内；在固定宽度整数实现里，这种写法还避免直接相加上下界造成溢出。若把大于分支误改为 high=mid-1，在 [1,2] 中找 1 就会跳过下标 0。此函数不扫描检查有序性，调用者负责建立这个前置条件。
测试与证明提供不同证据
“测试只能发现 bug，不能证明没有 bug”是过度概括。若输入域有限且测试穷尽全部状态，测试可以证明该模型范围内的性质；模型检查也能穷尽有限状态空间。问题在于真实系统的输入、时间和并发状态通常太大，测试覆盖只是其中一部分。
| 方法 | 强项 | 边界 |
|---|---|---|
| 单元/示例测试 | 具体行为、回归 | 覆盖有限 |
| 属性测试 | 大量生成输入、缩小反例 | 仍非一般穷尽 |
| 模糊测试 | 非预期输入和解析器缺陷 | 难表达完整功能规格 |
| 静态分析 | 无需运行覆盖多路径 | 抽象可能误报或漏报 |
| 模型检查 | 穷尽有限模型状态 | 状态爆炸、模型偏差 |
| 演绎证明 | 对规格建立通用保证 | 规格、工具和可信基也可能有错 |
可靠工程通常组合多种证据。证明核心算法不替代集成测试；测试外部依赖也不替代不变量推理。
规格错了，证明也会忠实地证明错事
证明工具只能判断实现是否满足给定模型。若规格漏掉“不能修改其他账户”，一个转账函数即使清空所有账户后设置目标余额，也可能满足过弱的局部后置条件。
规格评审应检查：
- 正常结果；
- 错误和异常；
- 未改变的状态；
- 边界与溢出；
- 终止和资源限制；
- 并发环境假设。
形式化的最大收益往往出现在写规格时：模糊需求被迫变成可讨论的条件。
完成检查
为“返回数组最大值”的函数完成：
- 写出空数组的处理方式和前置条件；
- 写出后置条件：结果属于数组，且不小于每个元素；
- 给出扫描循环的不变量；
- 给出终止变体；
- 说明整数类型、并发修改和异常是否在模型中；
- 设计示例测试、属性测试和一种静态或形式化检查。