算法正确性

测试只观察有限多次执行，规格中的量词却覆盖全部合法执行。结果符合规格通常靠不变量与归纳证明；终止性则靠某个进入良基关系并沿每一步严格下降的排名或变体。两项义务可独立失败，所以必须分开陈述。

二分查找公理库二分查找Binary search在有序数组中反复排除一半候选区间的查找算法。维护不变量“若目标存在，则位于当前区间 $[l,r)$”。区间空时，不变量说明目标不存在；每轮后 $r-l$ 严格下降则证明终止。若把更新写成 l = mid 而非 mid + 1，候选区间可能不再缩小：结果论证仍看似合理，终止义务却已失败。

while true do skip 没有终止执行，因而对任意 $P,Q$ 都真空地满足部分正确性，却不满足完全正确性。正确性也永远相对于规格：一份严密证明可以准确验证一条写错的规格，却不能替代对需求本身的确认。Collatz 迭代对所有正整数是否终止至今未知；对任意程序自动判定终止性更是不可能，这是停机问题公理库停机问题不可判定性Halting problem · Undecidability of halting不存在一个对任意程序和输入都能正确判断程序是否停机的算法。的直接边界。

循环不变式公理库循环不变式Loop invariant在循环初始化后成立，并在每次循环迭代后继续成立的断言。与 最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。把结果证明分解为可检查的局部义务，良基关系上的递减量公理库终止性与良基关系Termination · Well-founded relation · Ranking function用不存在无限下降链与严格递减排名函数刻画程序或转移系统的终止。负责终止。模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。若发现失败，可用反例轨迹见证某条允许执行违反规格；若给出证明证书，检查器也只是在核对证书相对于该规格是否成立。规格本身是否忠实表达需求，仍是另一项审查。

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