最弱前置条件

最弱前置条件把验证方向倒过来：先说执行后要什么，再沿程序逆向计算执行前恰好需要什么。“最弱”意味着不多要求任何无关事实，因而所有能保证目标的前置条件都蕴含它。赋值时无需模拟所有状态，只把后置公式中的变量替换为赋值右侧；顺序语句则从最后一条一步步向前。循环会形成递归方程，实际验证通常用不变量给出可证明近似，而不是自动得到精确闭式。

对命令 $x:=x+1$ 与后置条件 $x>0$，

在整数上即 $x>-1$。对 x:=x+1; y:=2*x 与目标 $y\ge 4$，先得第二步前置 $2x\ge 4$，再代回第一步得到 $2(x+1)\ge 4$，即 $x\ge 1$。

边界是非终止：总正确性的 wp 必须排除会发散的初始状态，而 wlp 可把这些状态视为平凡满足。对非确定程序，通常采用 demonic 解释，要求所有可能执行都终止并满足 $Q$；若采用 angelic 解释，量词会变成存在，得到不同谓词。

最弱前置条件把Hoare 三元组公理库Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。 $\{P\}C\{Q\}$ 转化为逻辑义务 $P\Rightarrow \mathrm{wp}(C,Q)$，是公理语义公理库公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。中自动验证条件生成的核心。条件语句产生分支公式，循环则需要不变量和终止变元。

它也把程序看成谓词变换器，为指称语义公理库指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。提供一种面向性质的模型。

SMT 驱动的验证器公理库基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。通常先用 wp 生成验证条件，再化简并求解背景理论公式；不变量发现、理论编码和求解分别有自己的可靠性边界。精化演算公理库精化演算Refinement calculus · Program refinement calculus以谓词变换器的精化次序和演算规则，从非确定规格逐步推导满足契约的可执行程序。则反向使用谓词变换器，从规格逐步选择能建立目标的程序构造。wp 仍是连接命令与后置条件的语义算子，不等同于求解器或程序合成策略。