Fa questo invariante di ciclo garanzia che la variabile non cambia mai?

Question

Supponiamo di avere un po 'di loop e ed intero k:

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

L'invariante di ciclo a (*) è: $ \ {K = k \} $

fa quella garanzia che $ k $ non cambia tra iterazioni? in caso contrario, non v'è alcun otherway garantire che?

Answer 1

L'invariante di ciclo non fa niente "garanzia". Si tratta di una sintesi delle informazioni rilevanti si sa sullo stato del programma quando si raggiunge quel punto. Se il ciclo è per esempio:.

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

in corrispondenza del punto k segnato == 5, ma non tutto il programma.