形式陈述

给定命令 $C$$C$ 和后置条件 $Q$$Q$，Dijkstra 的最弱前置条件 $\operatorname{wp}(C,Q)$$\mathrm{wp}(C,Q)$ 是保证 $C$$C$ 终止且终态满足 $Q$$Q$ 的最弱断言：

$$ \{P\}C\{Q\}\text{ 在总正确性意义下成立} \quad\Longleftrightarrow\quad P\Rightarrow\operatorname{wp}(C,Q). $$$$\{P\}C\{Q\}\text{ 在总正确性意义下成立}⟺P\Rightarrow \mathrm{wp}(C,Q).$$

“最弱”指它允许的初态集合最大。基本变换包括

$$ \operatorname{wp}(x:=E,Q)=Q[E/x],\qquad \operatorname{wp}(C_1;C_2,Q)=\operatorname{wp}(C_1,\operatorname{wp}(C_2,Q)). $$$$\mathrm{wp}(x:=E,Q)=Q[E/x],\mathrm{wp}(C_1;C_2,Q)=\mathrm{wp}(C_1,\mathrm{wp}(C_2,Q)).$$

只要求“若终止则满足”的偏正确性对应最弱自由前置条件 $\operatorname{wlp}$$\mathrm{wlp}$，两者不可混同。

直觉

从目标状态条件反向穿过程序，逐步计算所有必然安全并能完成执行的初始状态；任何更强前提只是额外排除了一些本来可行的状态。

例子与边界

对命令 x := x+1 和后置 $x>0$$x>0$，最弱前置是 $x+1>0$$x+1>0$，即 $x>-1$$x>-1$。对必不终止的命令，$\operatorname{wp}(C,Q)$$\mathrm{wp}(C,Q)$ 为假，因为没有初态保证终止；而 $\operatorname{wlp}(C,Q)$$\mathrm{wlp}(C,Q)$ 可为真。非确定选择的 wp 取决于恶魔式还是天使式语义，不能在未说明选择模型时固定为合取或析取。

推论与应用

wp 演算把程序验证化为公式变换，用于验证条件生成、程序推导和精化。其单调性、合取保持等健康性条件还可刻画命令语义，但循环通常产生不动点或需不变式近似。

参考资料

• C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Communications of the ACM 12(10), 1969，Full paper, assertion transformation implicit in axiomatic semantics。
• Edsger W. Dijkstra, A Discipline of Programming, Prentice Hall, 1976，Chs. 1–4, weakest preconditions and guarded commands。