When are invariants true inside of 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*}
&amp;s \gets 0  \\
&amp;i \gets |A| \\
&amp;\textbf{while } i &gt; 0 \textbf{ do} \\
&amp;\quad i \gets i - 1 \\
&amp;\quad s \gets s + A[i] \\
&amp;\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.