[Math] Purpose of Loop invariant

computer sciencediscrete mathematics

I have some small fairly easy questions regarding following procedure. My teacher has post some answers which I fairly understand but also have questions about. Note: I have taken a screenshot of the answer since it would be difficult to format the text which he wrote.

procedure sum(n: positive integer)  
  i := 1  
  x := 1  
  s := 1  
  while i < n  
    i := i + 1  
    x := x + 2  
    s := s + x  

  return s   

Assigment:

  1. Prove that the following assertion is a loop invariant for the while-loop:

$$i \in \mathbb N \land i \le n \land x = 2i−1 \land s=i^2 $$

  1. What is the value of $s$ in terms of $n$ when the algorithm terminates? Justify your answer.

My Question:

The things which I do not understand are marked with yellow which I hope that someone will take the time to explain.

1) I see that $$ s + x = i^2+2i+1. $$
But, I do not see how that is equal to $(i+1)^2$

2) Also, what is the purpose of the loop invariant? Is it to show that $1$ runs all the way in the loop or what?

enter image description here

Any comment is appreciated. Thank you for your kind help.

Best Answer

For (1):
if you expand $(i+1)^2$ you get $i^2+2i+1$.
You should know that, so I'm not sure if I interpreted your question correctly.

For 2):
Since $i_{new}=i+1$, $\;\;i^2_{new}=(i+1)^2$

What is a loop-invariant?
A loop-invariant is a statement that you can make about variables in a program that will be true at the end of each iteration of a loop.

For example, $i\in N$, $i\leq n$ and $s=i^2$ are all loop-invariants.

The purpose of a loop-invariant is to help you prove that a program is correct.
For example, suppose it is claimed that sum($n$) produces $n^2$ for all positive integers $n$.

First, you prove that $s=i^2$ is a loop-invariant using induction.

Next, you note that at the end of the $k^{th}$ iteration of the loop, we have $i=1+k$ and that the loop terminates after the $(n-1)^{th}$ iteration.

This means that when the loop terminates after $k = (n-1)$ iterations we have:

$s=i^2=(1+k)^2=(1+(n-1))^2= n^2$

Hope this helped.