プログラムの正当性

コンピュータ理論のひとつにホア論理というのがある。この論理の中心は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である。面白いのは、メイヤーが契約による設計原則に不変状態を追加している点である。