最弱事前条件の性質

$\mathcal{M}$ を解釈、$c, c_1, c_2$ を命令、$P, Q, Q_1, Q_2$ を表明とする。

1. （特徴づけ）$\models_{\mathcal{M}} \{P\}\ c\ \{Q\}$ は $P \Rightarrow \mathrm{wlp}(c, Q)$ と同値である。また $P \Rightarrow \mathrm{wp}(c, Q)$ ならば $\models_{\mathcal{M}} [P]\ c\ [Q]$ である。
2. （単調性）$Q_1 \Rightarrow Q_2$ ならば $\mathrm{wlp}(c, Q_1) \Rightarrow \mathrm{wlp}(c, Q_2)$ かつ $\mathrm{wp}(c, Q_1) \Rightarrow \mathrm{wp}(c, Q_2)$。
3. （連言）$\mathrm{wlp}(c, Q_1 \wedge Q_2) = \mathrm{wlp}(c, Q_1) \wedge \mathrm{wlp}(c, Q_2)$、$\mathrm{wp}(c, Q_1 \wedge Q_2) = \mathrm{wp}(c, Q_1) \wedge \mathrm{wp}(c, Q_2)$。
4. （選言）$\mathcal{M}$ がすべての操作名について部分関数ならば、$\mathrm{wp}(c, Q_1 \vee Q_2) = \mathrm{wp}(c, Q_1) \vee \mathrm{wp}(c, Q_2)$、$\mathrm{wlp}(c, Q_1 \vee Q_2) = \mathrm{wlp}(c, Q_1) \vee \mathrm{wlp}(c, Q_2)$。さらにこのとき、$\models_{\mathcal{M}} [P]\ c\ [Q]$ は $P \Rightarrow \mathrm{wp}(c, Q)$ と同値である。
5. （計算規則）$\mathrm{wlp}(\mathtt{skip}, Q) = Q$、$\mathrm{wlp}(x := a, Q) = Q[a/x]$、$\mathrm{wlp}(c_1; c_2, Q) = \mathrm{wlp}(c_1, \mathrm{wlp}(c_2, Q))$、 $\mathrm{wlp}(\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, Q) = \bigl(b \wedge \mathrm{wlp}(c_1, Q)\bigr) \vee \bigl(\lnot b \wedge \mathrm{wlp}(c_2, Q)\bigr)$。