述語変換意味論
述語変換意味論では、命令型プログラミング言語の意味論(プログラム意味論)を定義するため、その言語の各「コマンド」に「述語変換子; Predicate Transformer」を対応させる。「述語変換子」は、プログラムの部分について2つの述語を対応させる全体関数である。
逐次的命令型プログラミングの基本的な述語は、最弱事前条件 w p ( S , R ) {\displaystyle wp(S,R)} で表される。ここで S はコマンドのリスト、R は事後条件空間内の述語を意味する。この関数を適用することで R が真となって完了する S の最弱事前条件(weakest precondition)が得られる。以下に代入文の例を挙げる:
w p ( x := E , R ) = R E x {\displaystyle wp(x:=E,R)=R_{E}^{x}}
これはつまり、R の中の x を E に置換した述語が得られることを意味する。整数型変数 x と y について代入文の wp を正しく計算した例を以下に示す:
w p ( x := y − 5 , x > 10 ) = ( y − 5 > 10 ) = ( y > 15 ) {\displaystyle wp(x:=y-5,x>10)=(y-5>10)=(y>15)}