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?

2
Contributors
1
2
Views
8 Years
Discussion Span
Last Post by galagatron

Here's how the code works:

It produced two streams of numbers, the i's and the s's (where N is the length of each stream).

i_n = (0,1,2,3,4,5,...,N-1)
s_n=(0,1,4,11,18,29,...,s_{N-2} + 2(N-3) + 1)

So, for example, an invariant would be that s is always equal to the sum of twice the previous i value and 1 plus the previous s value.

To formally prove the correctness of the invariant, you need to do two things:
(1) Prove the base case, i.e., where i=s=0
(2) Prove the inductive step, going from s_{n-1} to s_{n)

Note that the invariant is often "trivially satisfied" at the base case, such as here where we can assert that i_{-1} = -1 and s_{-1) = 1, and therefore the invariant is satisfied before the first execution of the loop.

Hope that helps.

Edited by galagatron: .

This topic has been dead for over six months. Start a new discussion instead.
Have something to contribute to this discussion? Please be thoughtful, detailed and courteous, and be sure to adhere to our posting rules.