循环不变量证明

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

循环不变量为:

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

证明:

归纳基数:平凡。

感应步骤:

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