CODEWITHSUNDEEP
validationformal-verificationloop-invariantproof-of-correctness
Mox
Mox

Reputation: 13

How can the strongest loop invariant be found for this code?

I am trying to come up with a loop invariant for the following while-loop, but am having some trouble.

After the loop invariant is decided on, I would like to put together a proof tableau and show all intermediate assertions

ASSERT(k >= 0)
{i = 1;
 sum = 1;
 while (i <= k) { 
     sum = sum + 2*i + 1;
     i = i+1;
 } //end-while
}
ASSERT( sum == (k+1)*(k+1) )

Upvotes: 1

Views: 201

Answers (2)

PF. Castro
PF. Castro

Reputation: 144

Note that when it exists the loop the value of i is k+1, that is, a good invariant seems:

INV(1) = {1 <= i <= k+1}

INV(2) = {sum == i*i}

Upvotes: 0

politinsa
politinsa

Reputation: 3720

INV(1) = {sum == (n+1)*(n+1)}  
INV(2) = {0<=n<=k}

sum = 1 works for n = 0
Now try to prove that it does work for n+1 (if true for n), until n reaches k (in your case, my n is your i)

Upvotes: 1

Related Questions