Hoare 三元组

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

在无溢出的整数语义中，三元组 $\{x=n\}x:=x+1\{x=n+1\}$ 有效，其中 $n$ 是记录初值的逻辑变量，命令不能修改它。更弱的后置条件 $x>n$ 也有效，而 $x=n+2$ 无效。若使用有符号定宽整数，还须明确溢出规则，不能照搬整数上的结论。

赋值规则从后往前推条件：为了赋值后满足 $Q$，应在赋值前检查 $Q[x\leftarrow e]$。例如目标为 $x>5$，命令为 $x:=x+1$，代入得到 $x+1>5$，也就是整数初态下的 $x>4$。替换的是后置条件中表示新值的自由 $x$，不是先把程序状态真的执行一遍。

对 while true do skip，部分正确性三元组 $\{P\}C\{Q\}$ 对任意 $P,Q$ 都成立，因为不存在终止执行；若 $P$ 可满足，相应总正确性三元组不成立。总正确性通常还需一个在循环中严格下降、又不能无限下降的量来证明终止。

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

Hoare 三元组是公理语义公理库公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。的基本判断。最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。通常同时要求终止与后置条件；只要求“若终止则满足后置条件”的对应算子称为最弱自由前置条件（wlp）。对死循环，前者为假，后者为真，这正是两种正确性的区别。循环不变量把任意迭代次数上的性质压缩成初始化、保持和退出三个有限证明义务。

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