¿Este bucle invariante garantiza que la variable nunca cambia?

Question

Supongamos que tiene algún bucle y entero K:

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

El bucle invariante en (*) es: $ {k = k } $

¿Eso garantiza que $ K $ no cambia entre iteraciones? Si no, ¿hay alguna otra vía para garantizar eso?

Answer 1

El invariante de bucle no "garantiza" nada. Es un resumen de la información relevante que conoce sobre el estado del programa cuando llega a ese punto. Si su bucle es, por ejemplo,

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

en el punto marcado K == 5, pero no en todo el programa.