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