algorithm - 循环不变证明

Question

我遇到了一个问题，提出了后置条件并显示了这段代码的部分正确性。

{ 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 }

我不是在寻找答案，因为这是学校的作业，只是洞察力，也许是一些指向正确方向的东西。我已经构建了值表，并且无法提出循环不变量。

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

我知道循环的结果是 m 后面的完美正方形，但我不确定如何写。

一如既往，感谢所有帮助。

Answer 1

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