代入文の公理

ウィキペディア小見出し辞書

(A1) 代入文の公理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/21 02:23 UTC 版)

「ホーア論理」の記事における「(A1) 代入文の公理」の解説

{ 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 は成り立つ、 というように読む。