# Loop invariant for a while loop I need help understanding why the two statements I have underlined with red are correct. I am confused as to how we can get $n + 1$.

And how $i \le n$ is true when it says $i < n$ in the while.

• – Gilles May 22 '17 at 9:00
• What exactly do you need help with? Do you know the definition of a loop invariant? What's stopping you checking that the statement satisfies the definition of being an invariant for the particular loop in the exercise? – David Richerby May 22 '17 at 10:01
• i know that a loop invariant is a statement that is true at any time in the loop. What i don't understand is how s = i(n+1) is it supposed to mean that n will grow with 1 for each iteration? – Linexxlol May 22 '17 at 11:35

## 2 Answers

The loop invariant should hold before and after each iteration of the loop. In particular, it should hold before the loop starts and after it ends.

1. Why $i \leqslant n$: because this program checks $i$ first and only then adds $+1$ to it.

2. When $s := s + i + x$ is applied, $x = n - i + 1$. Substituting $x$ to original formula we get $s := s + n + 1$. It is equal to $(n + 1) i$.