代入の規則は後ろ向きである

$x$ を変数、$a$ を算術式、$P, Q$ を表明とする。解釈は任意でよい。

1. $\models \{Q[a/x]\}\ x := a\ \{Q\}$ が成り立つ。
2. $\models \{P\}\ x := a\ \{Q\}$ ならば $P \Rightarrow Q[a/x]$ である。すなわち $Q[a/x]$ は、事後条件 $Q$ を保証する事前条件のうちでもっとも弱い。
3. 「前向き」に書いた規則 $\{P\}\ x := a\ \{P \wedge x = a\}$ は正しくない。$P$ を $x = 0$、$a$ を $x + 1$ とすると、三つ組 $\{x = 0\}\ x := x + 1\ \{x = 0 \wedge x = x + 1\}$ は部分正当でない。