最弱自由前置条件

“liberal”不是降低后置条件，而是拒绝在同一个判断里承诺终止。它问的是：如果程序有一天返回，返回状态会不会违反 $Q$？这使安全性证明可以先独立于终止性开展。随后若另有排名函数、结构递归或其他终止证书，二者合在一起才成为总正确性。

最大不动点给出一个可靠的方向检查。对 while true do skip，无论后置条件是什么都没有终止结果，所以每个初态都满足 wlp；全集正是相应循环方程的最大解。若误取最小解，会把这个程序的 wlp 算成空集，悄悄把终止要求塞回部分正确性。

考虑整数程序

if x = 0 then
    while true do skip
else
    y := x

后置条件为 $y\ne 0$。当 $x\ne 0$ 时，赋值终止且建立后置；当 $x=0$ 时，唯一分支发散，没有违反后置的终止结果。因此

这两个结果的差异完全来自终止量词，而不是赋值规则。

对 demonic 选择 skip [] diverge，若当前状态满足 $Q$，wlp 为真，因为唯一终止结果仍满足 $Q$；wp 却为假，因为调度可以选择发散分支。若使用 angelic 选择，终止量词会变成“存在成功选择”，得到另一种变换器，不能沿用上述公式。

异常和 stuck 也必须分类。若除零被定义为错误终态，它应由单独的异常后置或安全条件约束；若把它误当作非终止，wlp 会平白放过内存错误。文献有时用 $wp$ 记部分正确性变换器，因此引用结论时必须同时核对语义定义，不能只看符号名称。

Hoare 部分正确性目标可改写为

对无循环命令，这给出最精确的安全入口条件；对带不变式的循环，验证器通常计算一个可证明的充分条件，而不是自动获得最大固定点的闭式表示。由此产生的初始化、保持与退出义务适合交给逻辑求解器检查。

wlp 也说明安全与活性为何必须分层：它对“坏结果永不出现”很自然，却无法区分正常完成与永远沉默。精化演算、程序验证器和异常逻辑若要组合这些结论，必须公开采用的是 liberal 还是 total 变换器，以及非确定选择由程序还是环境控制。