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?