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?
Does this loop invariant guarantee that the variable never changes?
loop invariants;program correctness;hoare logic
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.