[解決済み】ループ不変量って何？

質問

CLRSの「アルゴリズム入門」を読んでいます。第2章で、ループ不変量について書かれています。ループ不変量ってなんですか？

どのように解決するのか？

ループ不変量とは、簡単に言えば、ループの反復ごとに成立する述語（条件）のことです。例えば、単純な for というようなループがあります。

int j = 9;
for(int i=0; i<10; i++)  
  j--;

この例では、(すべての繰り返しにおいて)真である i + j == 9 . より弱い不変量も真であり、次のようになります。 i >= 0 && i <= 10 .