CODEWITHSUNDEEP
algorithmloopspost-conditionsloop-invariant
Ross Verry
Ross Verry

Reputation: 115

Loop invariant proof

I am running into an issue coming up with the post-condition and showing partial correctness of this piece of code.

{ m = A ≥ 0 }
  x:=0; odd:=1; sum:=1;
  while sum<=m do
    x:=x+1; odd:=odd+2; sum:=sum+odd
  end while
{ Postcondition }

I'm not looking for an answer, as this is an assignment for school, just insight and perhaps some pointing in the right direction. I have constructed the table of values, and cannot come up with the loop invariant.

x   odd sum m   (x + 1)^2   odd - x (odd - x)^2
0   1   1   30    1            1        1
1   3   4   30    4            2        4
2   5   9   30    9            3        9
3   7   16  30    16           4        16
4   9   25  30    25           5        25
5   11  36  30    36           6        36

sum = (odd - x)^2

I have that the outcome of the loop is the perfect square following m, but I'm not sure how to write that.

As always, all help is appreciated.

Upvotes: 3

Views: 1196

Answers (1)

Egor Skriptunoff
Egor Skriptunoff

Reputation: 23737

Loop invariant is: 

odd = 2x+1
sum = (x+1)^2

Proof:

Induction base: trivial.

Induction step: 

new_x = x+1
new_odd = odd+2 = 2(x+1)+1 = 2*new_x+1
new_sum = sum+new_odd = (x+1)^2+2(x+1)+1 = new_x^2+2*new_x+1 = (new_x+1)^2

Upvotes: 2

Related Questions