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.
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.
Why $i \leqslant n$: because this program checks $i$ first and only then adds $+1$ to it.
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$.