¿Este bucle invariante garantiza que la variable nunca cambia?
-
16-10-2019 - |
Pregunta
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?
Solución
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.
Licenciado bajo: CC-BY-SA con atribución
No afiliado a cs.stackexchange