算法正确性

测试只观察有限多次执行，规格中的量词却覆盖全部合法执行。循环不变量把这个无限要求拆成三个局部检查：进入循环前成立；假定某轮开始时成立，执行一轮后仍成立；退出时，不变量与退出条件一起推出后置条件。第二步以一轮为归纳步，把任意有限轮的状态连接起来。

这些检查仍没有说明循环一定退出。终止性还要找到一个落在良基集合中的变体，例如非负整数，并证明每轮严格下降。仅有“数值越来越小”不够：正实数序列 $1,1/2,1/4,\dots$ 可以无限下降。因此，不变量与递减量分别承担结果正确和执行终止的证明。

二分查找怎样分别证明答案与终止 ​

设输入数组非降序排列，搜索值为 $v$。二分查找公理库二分查找Binary search在有序数组中反复排除一半候选区间的查找算法。从 $l=0,r=n$ 开始，保持 $0\le l\le r\le n$，并保持“若数组含有 $v$，则当前区间 $[l,r)$ 至少含有一次出现”。当 $l<r$，令 $m=l+\lfloor (r-l)/2\rfloor$。若 $A[m]=v$ 就返回 $m$；若 $A[m]<v$，有序性说明所有下标不超过 $m$ 的值都太小，故更新 $l=m+1$；否则更新 $r=m$。每次删去的部分都不含目标，因此不变量得以保持。

退出时 $l=r$，候选区间为空，不变量便证明目标不存在。另一方面，循环开始时的整数 $r-l>0$，两种更新都让它严格下降，且始终非负，因此只能执行有限轮。这分别完成部分正确性与终止性。

例如在 $[2,5,9]$ 中查找 $7$，区间依次为 $[0,3)$、$[2,3)$、$[2,2)$，最后报告不存在。若在小于目标的分支错写 l = m，当区间只含一个小于目标的元素时会原地不动；被排除区域的论证仍可能成立，终止义务却已失败。

while true do skip 没有终止执行，因而对任意 $P,Q$ 都真空地满足部分正确性，只要 $P$ 允许至少一个初始状态，就不满足完全正确性。

规格审查还要确认 $Q$ 是否表达了实际需求：程序证明保证执行符合 $Q$，需求审查保证这个目标本身合适。

对任意程序自动判定终止性是不可能的，这是停机问题公理库停机问题不可判定性Halting problem · Undecidability of halting用总停机判断器的自反转构造证明 HALT 不可判定，并区分识别、有限步数检查与局部终止性证明。的直接边界。

循环不变式公理库循环不变式Loop invariant在循环初始化后成立，并在每次循环迭代后继续成立的断言。与 最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。把结果证明分解为可检查的局部义务，良基关系上的递减量公理库终止性与良基关系Termination · Well-founded relation · Ranking function用不存在无限下降链与严格递减排名函数刻画程序或转移系统的终止。负责终止。模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。若发现失败，可用反例轨迹见证某条允许执行违反规格；若给出证明证书，检查器则验证证书是否满足相应证明规则。证书算法公理库证书算法Certifying algorithm · Certificate-producing algorithm让求解器随答案输出可独立检查的证书，并用检查器的可靠性证明已接受结果满足规格的计算接口。把这种分工落实为求解器与独立检查器：接受一份证书能确认当前答案，却不能代替求解器对所有输入的终止证明。

当算法允许近似、随机错误或在线交互时，必须把扩展保证写进规格：近似算法说明允许的数值偏差，随机算法说明坏事件及其概率，在线算法固定输入揭示方式和比较对象。运行时间、空间与通信量描述计算成本，与输出规格一起构成算法的完整保证。非确定程序仍需覆盖所有允许执行；并发程序往往把完整调用—返回历史而非单个终态作为规格对象。