プログラムの正当性
コンピュータ理論のひとつにホア論理というのがある。この論理の中心はHoare Tripleという式である。
{P}C{Q}
この式はプログラム実行による状態変化を表す。CはPの状態に始まりQの状態で終わる。Cはコマンド、Pは事前状態、Qは事後状態である。
プログラムの正当性はこの命題が真かどうかで決まる。
例を示す。
{a<5}a=a+3{a<7}
これはa<5の時にコマンドを実行すると、コマンドが終わった時点ではa<7となる、という意味だ。もちろんこの命題は真である。但しa<8でも真である。この時、a<8はa<7よりも弱い状態であるという。もっとも弱い事後状態はa<8となる。
メイヤーが提唱する契約による設計原則のベースはこのHoare Tripleである。面白いのは、メイヤーが契約による設計原則に不変状態を追加している点である。