ホーア論理
{ Q[e/x] } x:=e { Q }
ここで、事前条件の Q[e/x] は置換であり、式 Q の中に出現するすべての x を式 e で置き換えた式を表す。一方で事後条件の Q は代入文実行後(置換ではなく代入を行ったあとの)x の値について式 Q が成り立つことを表す。
したがって、この公理は、
{ Q[e/x] }:式 Q 中の全ての x を e に置換するとき式 Q が成り立つのであれば、
x:=e:(置換で成り立つならば、ほぼ同じような代入操作でも変わらないはずのため)式 Q 中の x の値を代入 x:=e で変更することで、
{ Q }:(置換の場合は成り立っているのであるから x の値が e に変更されたのであれば当然に)代入文実行後の式 Q は成り立つ、
というように読む。