不変条件

ウィキペディア

不変条件

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2014/05/06 03:44 UTC 版)

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

用法

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

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

例

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

1. ある文字列が I で終わっている場合、U をそれにつなげることができる（xI → xIU）
2. Mの後の文字列は全体を複製できる（Mx → Mxx）
3. 3つの I が連続している場合（III）、それらを1つの U に置換できる（xIIIy → xUy）
4. 2つの U が連続している場合、それらを削除できる（xUUy → xy）

この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.

関連項目

• ホーア論理
• ループ不変条件

外部リンク

• Applet: Visual Invariants in Sorting Algorithms

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

不変条件

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/12/28 09:17 UTC 版)

「契約プログラミング」の記事における「不変条件」の解説

クラス不変条件 (class invariant) は、クラスが持つ公開された各メソッドの開始時と正常終了時に共通して保証されるべき状態についての条件である。ただしコンストラクタの呼び出しに関しては、事後条件としてのみ適用され事前条件として保証する必要はない。（引数や返り値などを制約するメソッド個別の事前/事後条件と異なり）不変条件はインスタンスの状態にのみに対する表明である。インスタンスの「状態」はそのインスタンスのすべてフィールドの値によって決まるため、より具体的には、不変条件はフィールドの値に関する表明となる。 不変条件は公開メソッドの事前条件および事後条件として暗黙的に追加される。不変条件を持つクラスに関して、そのクラスの公開メソッドの呼び出しの際、クライアントはメソッドの事前条件とサプライヤ・クラスの不変条件の両方を満たす義務がある。またサプライヤは、事前条件（と不変条件）を満たしたメソッド呼び出しに対して、メソッド終了時にそのメソッドの事後条件と不変条件の両方を満たす義務がある。