コンピュータ理論のひとつにホア論理というのがある。この論理の中心はHoare Tripleという式である。{P}C{Q} この式はプログラム実行による状態変化を表す。CはPの状態に始まりQの状態で終わる。Cはコマンド、Pは事前状態、Qは事後状態である。プログラムの…