述語変換意味論
この意味は、事後条件 x > 10 が代入実行後に真となるためには、事前条件として y > 15 が代入前に成り立っていなければならないことを示している。これも最弱事前条件であり、代入後に x > 10 を真とするために最低限必要となる y に対する条件である。
ダイクストラは他にも選択(if)や繰り返し(do)、接合演算子(;)を wp を使って定義した。選択や繰り返し構文はガード付きコマンドを使って実行を制御する。彼が wp の定義に課した規則により、コマンドのガードが互いに素でない場合、これらの構文では非決定的実行が可能になる。
他の形式主義的意味論とは異なり、述語変換意味論は計算の基礎を研究するような設計ではない。むしろ、プログラマが計算をするような感覚でプログラムの正しさを確認する手法を与えるものである。この手法はダイクストラらが提唱し、Ralph-Johan Back の Refinement Calculusで高階論理へと拡張された。
なお、逐次型プログラミングの意味論として最弱事前条件は広く認知されているが、これが唯一の述語変換子ではない。例えば、レスリー・ランポートは並行プログラミングのための述語変換子として win と sin を提唱した。