ループ不変条件

ループ不変条件（英: Loop invariant）とは、計算機科学において、ループの不変条件のこと。ループとは、繰り返し実行されるコードのこと。ループの不変条件とは、ループ実行前にも、反復を実行するたびにも成立する条件のこと。これは、論理アサーションであり、アサーションを使ってコードが書かれることもある。不変条件を知ることは、ループの意味を知るのに重要である。

形式的検証において、特にホーア論理を使った方法では、ループ不変条件は形式的な述語論理で表現され、ループの特徴やループのアルゴリズムを証明するのに使われる。ループ不変条件はループに入る前の段階でも真であり、ループを繰り返すたびにも真である必要がある。これは、ループが終了する際には、ループ不変条件とループ終了条件の両方が真であることが保証される。

ループと再帰の基礎的な類似性により、ループ不変条件を使いループの部分的な正しさを証明するのと、再帰プログラムを構造的帰納法を使い証明するのは、非常に類似している。事実、ループ不変条件は、たいていは、ループと等価な再帰的プログラムで証明しないといけない帰納法の仮説と同じである。

非形式的な例

下記C言語の関数 max は配列 a[] の最大値を返す。n は配列の長さで、1以上とする。行番号 3, 6, 9, 11, 13 のコメントはその場所で成立している性質。行番号 6, 11 はループ不変条件。行番号 13 はループ不変条件とループ終了条件が両方とも成立している。

int max(int n, const int a[n]) {
    int m = a[0];
    // m は a[0...0] の最大値
    int i = 1;
    while (i != n) {
        // m は a[0...i-1] の最大値
        if (m < a[i])
            m = a[i];
        // m は a[0...i] の最大値
        ++i;
        // m は a[0...i-1] の最大値
    }
    // m は a[0...i-1] の最大値、かつ、i == n
    return m;
}

関連項目

• 不変条件
• 数学的帰納法