这一段代码的归纳不变式是什么？

Question

对于这段代码：

  // n is a user input that can be any integer
  s = 0
  i = 0

  while i < n:
    s = s + 1
    i = i + 1

  return s

我想证明后置条件为if n > 0 then s = sum(0, n) else s = 0，其中sum(s,e)只是从s到e包括1，从初始值0开始。

我以为不变是if n > 0 and i < n then s = sum(0, i) else s = 0，但我无法在Coq或z3中得到证明。有任何提示吗？

Answer 1

您似乎暗示此算法会计算总和，但实际上并没有这样做。相反，它将最多计为n。也许您想要的是：

i = 0
s = 0
while i < n:
  i = i+1
  s = s+i

请注意，我们将s增加了i，而不是您程序中的1。

假设这是预期的程序，那么好的不变式将是：

• [s是所有数字的总和，包括i
• [i最多为n] >>

以其他程序化表示法：

s == i*(i+1)/2 && i <= n
要了解原因，请记住，在每次循环迭代之前和之后必须保持不变；当循环条件为假时，则需要暗示您的后置条件。这就是为什么需要连接词i <= n的原因，所以当退出循环时，s确实包含和。