我怎样才能找到循环不变量并证明正确性？

Question

我正在学习正确性并努力寻找合适的循环不变量并证明其正确性。

我认为循环不变量应该是正值的 t=sum，但我不知道如何正确编写它或者是否有任何其他循环不变量？

SumPos(A[0..n - 1])
// Returns the sum of the positive numbers in an array A of length n. We
// assume that the sum of the numbers in an array of length zero is 
zero.
t = 0
i = 0
while i != n do
 if A[i] > 0
 t = t + A[i]
 i = i + 1
 return t

Answer 1

在正式开始之前，有时考虑一下“什么保持不变”和“什么变化”关于循环会很有帮助。* 对于编写的循环，我们有以下变量兴趣：

• A - 要求和的数字数组
• n - A 中的整数个元素。
• t - 如所写，我认为打算成为最终的阳性总和
• i - 索引变量；有时称为变体

那么每次迭代都会发生什么变化？数组A 不会改变。数组中元素n 的数量不会改变。如所写，总和 t 可能会改变。索引变量i将改变。

那么，关于循环，人们通常会说i 是变体。它会增加每次迭代，并将其与 n 进行比较是退出循环的内容。

我感兴趣的不变量是t 将始终代表计算出的迄今为止的阳性总和。例如，在第一次迭代中：

• 迭代前i == 0和t也正确为0
• 迭代后，i == 1 和 t 将相对于第一个元素正确。

但是，正如所写，return 语句排除了数组第一个元素之外的任何处理。从理论转向实践，那么您将如何修复实现？

* 对于迂腐的人来说，限定符很重要，因为严格来说，“不变量”是不会改变的东西——不会改变，或者总是成立——对于循环的每次迭代。所以？ 很多语句对于循环是不变的！例如，我妈妈的名字在循环中是不变的！