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?
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.
constantmodifier that many imperative languages come with. If you want to be explicit in your Hoare logic about it, then you can reference the new updated value or the old value and indicate that they are the same. For example, in the Z formalism, you would writek = k'which says updated valuek'is identical to original valuek. Another example would bek == \old(k)if you were using Frama-C. $\endgroup$