如何证明这个while循环计算n^2

Question

本周晚些时候，我正在为我的逻辑学考试做准备，我必须证明这是while循环：

i := 0
s := 0
while i < n do
    i := i + 1
    s := s + (2*i -1)

计算n^2。这个问题由两个子问题组成。我们必须证明0≤i≤n∧S= i^2是这个while循环的循环不变量。我成功地证明了这一点，但第二个子问题是，我必须证明这个循环计算n^2，但我不知道如何开始。这门课对问题的这一部分有点混淆。

Answer 1

循环计算1+3+5+7+.+ (2n-1)。最简单的方法来想象这个和为n^2是

Answer 2

使用算术级数公式，我们可以直接导出它：

元素数为n，第一个元素为1，最后一个元素为2*n-1。

n*(1 + 2*n-1)/2 = n*(2*n) /2 = n*n

Answer 3

现有的答案漏掉了一个重要的问题:作业已经证明了一些事情，而练习试题要求他先证明这些事情。据推测，这是因为他已经证明了的东西是为完成这一证明提供方便的垫脚石。

我们要证明程序输出n^2。由于没有输出语句，因此可能有一个变量是输出，并且它不是i，所以它必须是s。

我们已经有了s=i^2，所以我们实际上已经非常接近了；如果循环的末尾是i=n，那不是很好吗？结果，在循环结束时，i=n是真的。我们就完蛋了。

在证明事情的时候，看看其他我们已经证明过的东西和我们想要证明的东西，往往是很有帮助的。我们拥有的东西和我们想要的东西的相似之处可以暗示我们要尝试的东西。