Consider the following program segment:

i := 0; s := 0;

while i<N do

begin

s := s + (2*i)+1;

i := i + 1;

end;

a.) What is the loop invariant, i.e., what assertion, if initially true

at the top of the loop, will remain true when execution reaches the

bottom of the loop?

b.) Try to show formally that if this assertion holds right after "begin",then it also holds just before "end" (and thus would always hold at thetop of the loop for each trip around the loop).

Hint: Since this is an invariant (or we hope it is), we know what we

want at both ends of the loop. So we can assume the invariant

at the top and work forward, or assume it at the bottom and

work backward. I suggested in lecture that going forward is

tricky, but gave a simple rule for going backward.

c.) Derive the assertion that must be true at the beginning of the

program in order to guarantee that the loop invariant is true

just before the while-loop.

Here is my attempt:

input N;

R= { 0=0} true

i := 0;

Q={ 0=i^2}

s := 0;

P= {s=i^2}

while i<N do

begin

P''={s=i^2}

s := s + (2*i)+1;

P'={ s = (i+1)^2}

i := i + 1;

P = { s = i^2}

end;

Correctness = { P and ~B , I < N}

P: S=i^2

~B: i>=N

so S>=N^2

I worked from bottom to top, so I assumed P.

(letters in red are my work)

Im not to sure if my assertion P holds with {while i<N do}.

Can someone check if my work is valid?

Also an explanation to how the code is executed/ how it works would be helpful?