不変条件

不変条件（英: invariant）とは、コンピュータプログラムの理論における用語で、ある処理の間、その真理値が真のまま変化しない述語 (predicate) であり、その処理シーケンスに対して不変であるという。

用法

コンピュータプログラムは一般にそれを実行したときの変化で表されるが、プログラムの不変条件が何であるかを知ることも同様に重要である。これは特にプログラムについて推論するときに便利である。コンパイラ最適化の理論、契約プログラミングの方法論、プログラムの正しさを判定する形式手法など、いずれもプログラムの不変条件を重視している。

プログラマはコード内でアサーションをよく使い、不変条件を明確化する。一部のオブジェクト指向プログラミング言語にはクラス不変条件 (class invariant) を指定する特別な構文がある。

論理問題での不変条件の特定が便利であることを示すため、MUパズルを例に用いる。このパズルは次の規則からなる。

この4つの規則だけで MI から MU に変換できるか、というのがダグラス・ホフスタッターの考案したMUパズルである。

このパズルをやってみると何時間でもつぶすことができるかもしれない。しかし、全ての規則に対して不変である述語を探し、MU を作ることができないと示す方が早い。論理的に見てみると、I を取り除くには I が3つ連続していなければならない。このことから、次のように興味深い不変条件が導かれる。

文字列内の I の個数は 3 の倍数ではない

この条件が不変条件と言えるのは、この条件が事前に成り立っている場合に、どの変換規則を適用した後も常に同じ条件が成り立っていると言える場合である。各変換規則が I と U の個数に与える効果を見てみると、この条件が不変条件だとわかる。

規則	Iの個数	Uの個数	不変条件への影響
1	+0	+1	I の個数は変化しない。不変条件が成り立っているなら、依然として成り立っていると言える。
2	×2	×2	n が3の倍数でない場合、2×nも3の倍数でない。不変条件は依然として成り立つ。
3	−3	+1	n が3の倍数でない場合、n-3も3の倍数でない。不変条件は依然として成り立つ。
4	+0	−2	Iの個数は変化しない。不変条件が成り立っているなら、依然として成り立っていると言える。

上の表を見れば明らかなように、この不変条件はどの変換規則を適用した後も成り立つ。したがって、最初に I の個数が3の倍数でないなら、どの規則をどういう順序で適用しても I の個数は3の倍数にはならない。

MI という文字列には I が1つしかなく、3の倍数ではない。MU には I が 0 個あり、0は3の倍数である。したがって、MI から MU への変換は不可能である。

C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259 | Download PDF
J.D. Fokker, H. Zantema, S.D. Swierstra (1991). "Iteratie en invariatie", Programmeren en Correctheid. Academic Service. ISBN 90-6233-681-7.