Garantiert diese Schleife invariante, dass sich die Variable nie ändert?

Question

Angenommen, Sie haben eine Schleife und und Ganzzahl k:

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

Die Schleife invariante bei (*) lautet: $ {k = k } $

Hat das garantiert, dass sich $ k $ zwischen Iterationen nicht ändert? Wenn nicht, gibt es einen anderen Weg, um das zu garantieren?

Answer 1

Die Schleifeninvariante "garantiert" nichts. Es handelt sich um eine Zusammenfassung der relevanten Informationen, die Sie über den Status des Programms kennen, wenn es diesen Punkt erreicht. Wenn Ihre Schleife zB ist:

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

am markierten Punkt k == 5, aber nicht überall im Programm.