总正确性 Hoare 逻辑

不变式回答“走到任何一轮都没有偏离正确区域”，变式回答“还剩多少不能无限消耗的进度”。一项是护栏，另一项是倒计时。倒计时不必是运行时间的精确估计，只需每次实际继续循环时落到更小的良基元素。

自然数适合单阶段循环；嵌套阶段可能需要字典序对、多重集合序或序数。复杂值域并不会自动带来证明，仍要展示每个程序分支严格下降。反过来，若某些步骤保持度量不变，就必须证明它们之间不能无限停顿，或换用能同时记录阶段与大小的组合变式。

例如外层剩余任务数为 $m$、当前任务内部剩余步数为 $k$ 时，可用字典序 $(m,k)$：内部步保持 $m$ 并减小 $k$，完成任务后严格减小 $m$，即使新任务的 $k$ 重新变大，整个二元组仍下降。只取 $m+k$ 未必成立，因为切换任务时 $k$ 可能大幅增加。

用重复减法计算非负整数除法：

q := 0
r := n
while r >= d do
    r := r - d
    q := q + 1

前置为 $n\ge 0\wedge d>0$，取

初始化显然成立。若 guard 为真，则新值 $q^{\prime }=q+1$、$r^{\prime }=r-d$ 满足

guard 给 $r^{\prime }\ge 0$，而 $d>0$ 给 $r^{\prime }<r$，所以自然数变式严格下降。退出时 $r<d$，结合不变式得到 $n=qd+r$ 与 $0\le r<d$，即商余数规格；这份证明同时承担功能与终止，而不是把“不断减”当作口头结论。

若允许 $d=0$，变式不下降；若使用无符号机器整数且减法可回绕，$r-d$ 的自然数论证也不再适用。随机程序的几乎必然终止只排除概率正的永久发散集合，不等于每条样本路径终止。并发线程即使局部变式下降，也可能因永远得不到调度而不结束，需另加公平性或进展逻辑。

总正确性把安全证明与终止证书组合为可复查的规则。递归过程可用参数上的良基下降替代循环变式；项重写系统用简化序；自动终止分析则尝试合成线性、词典序或分段排名函数。合成器没有找到候选，只说明当前模板失败，不是程序必然发散。

验证工具还必须区分正常返回、异常、stuck 与非终止。若异常属于接口允许的完成方式，需要相应后置条件；若目标要求正常返回，异常路径就是总正确性反例。性能上“很慢”和逻辑上“必终止”也是不同结论：良基证明不提供实用时间界，除非进一步量化每次下降的成本和初始度量。

总正确性也有可组合性侧面：顺序 $C;D$ 要先证明 $C$ 从前置出发终止并建立中间断言，再证明 $D$ 从每个这样的中间状态终止。若 $C$ 只在某一条幸运路径建立 $D$ 的前置，存在性执行不能满足总正确性的全称语义。