このループ不変は、変数が変わらないことを保証しますか？

Question

ループと整数kがあるとします。

int k = 5;
for (int i = 0 ; i < N; i++)
{
  //(*)
  //do something 
}

（*）のループインフアイアントは：$ {k = k } $です

それは、$ k $が反復の間に変化しないことを保証しますか？そうでない場合、それを保証する別の方法はありますか？

Answer 1

ループの不変は、何も「保証」しません。これは、プログラムがそのポイントに到達したときに、プログラムの状態について知っている関連情報の要約です。ループの場合：

k = 5;
...
for(int i = 0; i < N; i++) {
   /* Invariant: k = 5 */
   ...
   k = 207;
   ...
   frob_very_hard(&k);
   ...
   k *= 3;
   ...
   k = 5;
}

マークされたポイントk == 5では、プログラム全体ではありません。