ループ不変条件（）とは、計算機科学において、ループの不変条件のことである。ループ不変条件とは、ループの実行開始前および各反復の前後において常に成立する論理的条件のことであり、アサーションを用いてコード中に明示されることもある。不変条件を把握することは、ループの意味を理解するうえで重要である。
形式的検証において、特にホーア論理を用いる手法では、ループ不変条件は形式的な述語論理で表現され、ループの性質やアルゴリズムの正しさを証明するために用いられる。ループ不変条件はループに入る前にも真でなければならず、また各反復を経るたびにも真を保たなければならない。これにより、ループが終了する際にはループ不変条件とループ終了条件の両方が成立することが保証される。
ループと再帰の基本的な類似性から、ループ不変条件を用いてループの部分的正しさを証明することと、構造的帰納法を用いて再帰的プログラムを証明することは、非常に類似している。実際、ループ不変条件は概して、そのループと等価な再帰的プログラムにおいて証明すべき帰納法の仮説と一致する。
非形式的な例 下記のC言語の関数 max は、配列 a[] の最大値を返す。n は配列の要素数であり、1 以上とする。行番号 3, 6, 9, 11, 13 のコメントは、その位置で成立している性質を示す。行番号 6 および 11 がループ不変条件であり、行番号 13 ではループ不変条件とループ終了条件の両方が成立している。
int max(int n, const int a[n]) { int m = a; // 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; }
関連項目 不変条件 数学的帰納法