形式陈述

给定前置条件 $P$、程序 $C$ 和后置条件 $Q$，部分正确性表示：若 $P$ 成立且 $C$ 终止，则终态满足 $Q$。完全正确性还要求 $C$ 对所有满足 $P$ 的输入都终止。

直觉

测试只能观察有限样例；正确性证明要覆盖整个输入域，并把“结果对”与“最终会得到结果”分开处理。

例子与边界

二分查找需证明返回的位置确实匹配或元素不存在，同时证明搜索区间严格缩小。一个永不终止的程序可真空地满足某些部分正确性断言，却不完全正确。

推论与应用

循环不变式、归纳证明、Hoare 逻辑和形式验证都是建立正确性论证的方法。

参考资料

• Thomas H. Cormen et al., Introduction to Algorithms, 4th ed., §2.1–2.2.
• Edsger W. Dijkstra, A Discipline of Programming, Chapter 4.