Does this loop invariant guarantee that the variable never changes?

Question

Suppose you have some loop and and integer k:

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

The loop invariant at (*) is: $\{ K=k\}$

Does that guarantee that $k$ doesn't change in between iterations? if not, is there any otherway to guarantee that?

Answer 1

The loop invariant doesn't "guarantee" anything. It is a summary of relevant information you know about the state of the program when it reaches that point. If your loop is e.g.:

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

at the marked point k == 5, but not all over the program.