# Does this loop invariant guarantee that the variable never changes?

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?

• You can indicate that a varaible does not change value by using a constant modifier 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 write k = k' which says updated value k' is identical to original value k. Another example would be k == \old(k) if you were using Frama-C. – Musa Al-hassy Apr 11 '16 at 18:19

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.

• I see. Is there any invariant I can add to the body of the loop that would hold iff k is not changed in the body of the loop? – Shmoopy Apr 12 '13 at 16:33
• This are comments for the human reader, so you can write the invariants as you wish. But if you care that k does have a specific value at a particular point of the loop, state it that way where it matters. – vonbrand Apr 12 '13 at 16:35
• @Shmoopy Use constants; many languages provide these. – Raphael Apr 12 '13 at 23:05