最弱前置条件

最弱前置条件（weakest precondition）是程序语义中的谓词变换概念。给定程序S和后置条件Q，wp(S,Q)描述恰好那些能够保证程序终止并在结束时满足Q的初始状态。它将“执行后想要什么”转换为“执行前必须满足什么”，不是经验上随手列出的几个检查项。

如果另一个条件P也足以保证同一结果，就应有P蕴涵wp(S,Q)。这就是最弱性的含义：它不排除任何本来能够保障目标的初始状态。例如x≥5蕴涵x≥0，前者更强，因为允许的状态更少。公式更短、涉及变量更少，均不自动等于逻辑上更弱。

参考：[1]

先假定变量取数学整数，表达式无副作用且总能求值。对赋值x:=e，最弱前置条件是在Q中以e安全替换x的自由出现，记作Q[e/x]。若要求执行x:=x＋2后有x>5，则逆推得到x＋2>5，即初始x>3；不是要求原来就满足x>5。

替换操作必须保持变量作用域，不能让原本自由的变量意外被量词绑定。若实际语言涉及溢出、除零、指针别名或异常，简单整数赋值模型也要相应扩充。最弱前置条件总是相对于明确的程序语义，不是对所有语言都适用的纯文本替换技巧。

参考：[2]

对顺序程序S1;S2，先求S2为达到Q需要什么，再把这个条件作为S1的后置条件，即wp(S1,wp(S2,Q))。例如x:=x＋1; y:=2×x，目标为y>10。先逆推后句得到2×x>10，再逆推前句得到2×(x＋1)>10；在整数模型下等价于初始x≥5。

对确定性的if B then S1 else S2，条件为(B蕴涵wp(S1,Q))且(非B蕴涵wp(S2,Q))。这里B必须按分支选择时的状态解释。若换成允许多个守卫同时成立的非确定性命令，还要保证至少一个分支可执行，并且所有允许被选择的分支都足以达到目标，不能只挑其中表现最好的一条。

参考：[2]

最弱自由前置条件wlp只保证：如果程序终止，结束状态就满足Q。它不承担终止义务，因此通常弱于wp。对于永远循环且不返回的程序，任意后置条件的部分正确性要求都不会被一个错误终态反驳；相应wlp可以为真，而要求真正完成任务的wp为假。

含循环时，完整最弱条件未必容易计算或在选定断言语言中表达。实践中常用循环不变式先证明部分正确性，再另证终止，或者寻找一个足够但不一定最弱的前置条件。能机械生成验证条件，不等于能自动解决每个条件；必须分清语义上的最弱条件、工具算出的近似条件与最终完成的证明。

参考：[1] [2]