最弱前置条件

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

对命令 $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 解释，量词会变成存在，得到不同谓词。

循环展示了结果保证与终止保证的区别。对整数程序 while x>0 do x:=x-1 和目标 $x=0$，初值 $x\ge 0$ 恰好足够：正数逐步降到零，负数则直接退出且违反目标。验证时可取不变量 $x\ge 0$，并用 $x$ 作为非负、每步严格下降的终止变元；不变量解释退出后的结果，变元解释为什么能退出。

按本页约定，总正确性 Hoare 三元组理路Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。等价于逻辑义务 $P\Rightarrow \mathrm{wp}(C,Q)$。若使用 Hoare 页默认的部分正确性，则对应 $P\Rightarrow \mathrm{wlp}(C,Q)$；不能在转换中悄悄加入或丢掉终止要求。它们都可用于公理语义理路公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。中的验证条件生成：条件语句产生分支公式，循环部分正确性使用不变量，总正确性还需终止变元等证据。

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

SMT 驱动的验证器理路基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。可按所验证的正确性口径生成相应条件，再化简并求解背景理论公式；只验证安全性或部分正确性的工具，不因此证明终止。不变量发现、理论编码和求解分别有自己的可靠性边界。精化演算理路精化演算Refinement calculus · Program refinement calculus以谓词变换器的精化次序和演算规则，从非确定规格逐步推导满足契约的可执行程序。则反向使用谓词变换器，从规格逐步选择能建立目标的程序构造。

最弱前期望理路最弱前期望Weakest preexpectation · Quantitative weakest precondition把输出奖励反向传过概率程序，推导赋值、概率分支和循环规则，并计算终止概率与未归一化期望。把后置布尔谓词推广为非负奖励函数：赋值仍作替换，概率分支使用加权平均，循环取最小不动点。后奖励一读出终止概率，而不是期望运行时间；对非终止路径的约定也必须与本页总正确性或部分正确性区分一致。