# When are invariants true inside of a loop?

It can make an algorithm or loop show a high level of certainty / confidence that the code is correct, such as in the case of a binary search, as described in the book Programming Pearls, 2nd Ed.

Are invariants true at most part of the loop and can be untrue at some part? That is, in the middle of the loop:

while a <= b
if (...)
// Point A
else
// Point B
end
// Point C
end


is it true that at Point A or Point B, something can change that cause the invariants to break, and it depends on the next iteration to "correct the invariants"? The same with Point C, something can change that can cause the invariants to break?

Maybe Point C is more likely the place where the invariants may break, as it is getting ready for the next iteration? So if it is a for-loop:

for(i = 0; i < n; i++) {
// ...
}


then the i++ is a place where the invariant may break? I am looking if there is any rule that says what time may invariants not hold true, or should they always hold true?

It seems for binary search, the invariants are always true, while for mergesort or quicksort, the invariants are only true at a certain point, such as for mergesort, the array is divided into 2, and it is in sorted order, but this invariant is only true only after the code recursively calls itself to sort both the left and right subarrays. But this is recursion, so I don't know if there is any difference between that or just a loop.

Are invariants true at most part of the loop and can be untrue at some part?

Invariants hold prior and after each execution of the loop body; there are no requirements for what happens in between its statements. Not only that, I would even say it is quite the norm that invariants are broken during the loop. Fixing them is actually a sort of programming paradigm; it gives you a way of determining what the values for variable assignments in a loop should be. In fact, this is a quite natural concept if your design approach is based on invariants (e.g., if you are writing programs which are annotated with JML as in design by contract and similar ideas based on formal proof systems).

For instance, consider the following toy example in which we want to sum over the elements in an array $$A$$ and save the result in the variable $$s$$:

\begin{align*} &s \gets 0 \\ &i \gets |A| \\ &\textbf{while } i > 0 \textbf{ do} \\ &\quad i \gets i - 1 \\ &\quad s \gets s + A[i] \\ &\textbf{done} \end{align*}

The invariant is $$s = \sum_{j=i}^{|A|-1} A[j]$$, and it holds prior and after each execution of the loop body. However, after $$i \gets i - 1$$ is executed, the invariant no longer holds, that is, we then have $$s = \sum_{j=i+1}^{|A| -1} A[j]$$. Hence, the next instruction updates $$s$$ so that the invariant holds again.

• invariants hold prior and after the loop but not inside? I re-read Programming Pearls and it seemed like the invariants are added as a line inside the loop as "mustbe".... so it is like an assert, I think. So if viewed this way, invariant is at a certain location, and while it might be true else where, there is no guarantee. I think you can state that it is true throughout the loop, such as one of the invariants for binary search: the range [low, high] inclusive includes the index of target, if target exists in the array, until $low > high$, then target doesn't exist. – nopole Aug 28 '19 at 17:09
• @太極者無極而生 No. An invariant holds before and after the loop, not necessarily in between. See, for example, here. Actually, most certainly will the invariant be broken somewhere in the middle of the loop (unless it is possible to execute multiple assignments in an atomic fashion); otherwise, the invariant would be completely independent from the variables which are modified within the loop and, hence, simply trivial. – dkaeae Aug 29 '19 at 7:21
• it seems it is "after and before" each iteration of the loop... or perhaps except some special point. That article you quoted points to en.wikipedia.org/wiki/Loop_invariant and the Informal example section actually has some invariants stated inside the loop... didn't expect a wiki article that actually talks about loop-invariant... that'd be quite useful to help improve the correctness of code – nopole Aug 29 '19 at 13:26
• @太極者無極而生 Aha. It seems the misunderstanding is coming from what the "loop" is supposed to be. What I intend to say is that the invariant holds before and after each execution of the loop body (and not that it holds before and after the execution of the entire while block). Let me also update the answer to render this more explicit. – dkaeae Aug 29 '19 at 13:52