When are invariants true inside of a loop?

Question

I am new to the idea of invariants and hope to find more information about it.

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.

Answer 1

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.