Hoare 三元组

三元组是一份条件契约：调用者提供 $P$，程序在终止时承诺 $Q$。它不要求 $Q$ 完整描述最终状态，只需陈述当前证明关心的事实；未提及的变量可能改变。部分正确性中的“若终止”是最容易被忽略的量词，死循环可以平凡满足许多三元组。前置条件为假时也没有合法初始状态，因此三元组真但没有实际运行内容。

三元组 $\{x=n\}x:=x+1\{x=n+1\}$ 有效。更弱的后置条件 $x>n$ 也有效，而 $x=n+2$ 无效。对 while true do skip，部分正确性三元组 $\{P\}C\{Q\}$ 对任意 $P,Q$ 都成立，因为不存在终止执行；相应总正确性三元组则通常不成立。

边界是并发或异常：普通顺序三元组未说明其他线程可否修改状态，也未说明异常出口。需要并发分离逻辑、原子规范或带多个后置条件的扩展，才能准确覆盖这些行为。

Hoare 三元组是公理语义公理库公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。的基本判断。最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。为给定 $C,Q$ 计算最精确的调用条件，循环不变量则把无限迭代压缩成有限证明义务。

分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。把 $P,Q$ 解释为堆资源并通过框架规则实现局部推理。函数契约和 API 规范都可看作三元组的工程化形式；SMT 软件验证公理库基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。则把赋值、分支和不变式规则产生的条件交给求解器。三元组的语义有效性量化所有满足 $P$ 的运行，求解器只回答某个编码公式是否有反模型，因此编码与规则的可靠性仍是独立证明义务。