3

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.

Daniel Daranas
  • 22,454
  • 9
  • 63
  • 116
Ross Verry
  • 115
  • 8
  • If you see that the sequence of sums is the same as the sequence of perfect squares, what else do you need? Is that the post condition you're looking for? Do you just need help proving it or something? – Kyle Strand Apr 20 '13 at 02:36
  • Well, that's what I had as my post condition initially, the `sum = (odd - x)^2`. I took that out though because I wasn't sure if that should instead be part of the loop invariant. I do need help proving it, but I don't want the answer outright. I think what I'm having the most trouble with is just finding the loop invariant. – Ross Verry Apr 20 '13 at 03:05
  • 1
    I prefer `sum = (x+1)^2`, but they're equivalent. The loop invariant is, I'd assume, the inductive step in the proof that the postcondition is true: in other words, given that `sum[n] = (x[n]+1)^2` for some `n`, the loop invariant is that `sum[n+1] = (x[n+1]+1)^2`. – Kyle Strand Apr 20 '13 at 03:22

1 Answers1

2

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
Egor Skriptunoff
  • 23,359
  • 2
  • 34
  • 64
  • I have to go through the steps and prove the loop invariant true during all three steps: Initialization, preservation, and completion. `{ m = A ≥ 0 } ⊃` `{ m = A ≥ 0 ∧ 1 = 1 ∧ 1 = (1)^2 }` `x = 0` `{ m = A ≥ 0 ∧ 1 = 2x + 1 ∧ 1 = (x + 1)2 }` `odd = 1` `{ m = A ≥ 0 ∧ odd = 2x + 1 ∧ 1 = (x + 1)2 }` `sum = 1` `{ m = A ≥ 0 ∧ odd = 2x + 1 ∧ sum = (x + 1)2 }` These are the steps for proving initialization, I think. – Ross Verry Apr 22 '13 at 14:43