我正在学习正确性，并努力找到合适的循环不变性并证明其正确性。
我认为循环不变量应该是正值的 t=和，但我不知道如何正确编写它，或者还有其他循环不变量吗？
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
在正式化之前，有时考虑循环的"什么保持不变"和"什么变化"是有帮助的。 对于编写的循环，我们有以下感兴趣的变量：
A- 求和的数字数组n-A中元素的整数。t- 如所写，我假设打算成为最终的正数总和i- 索引变量;有时称为变体
那么每次迭代都会发生哪些变化呢？ 数组A不会更改。 数组中n元素的数量不会更改。 如前所述，t总和可能会发生变化。 索引变量i将更改。
至于循环，那么，人们通常说i是变体。 它增加每次迭代，将其与n进行比较是退出循环的原因。
我感兴趣的不变性是，t将始终表示迄今为止计算的正数总和。 例如，在第一次迭代中：
- 迭代前，
i == 0和t也正确为 0 - 迭代后，
i == 1和t对于第一个元素将是正确的。
但是，如前所述，return 语句排除了数组第一个元素之外的任何处理。 从理论到实践，那么如何解决实施问题呢？
* 对于迂腐的人来说，限定词很重要，因为严格来说，"不变"是不会改变的东西 - 不会改变，或者总是成立 - 对于循环的每次迭代。 所以？许多语句对于循环是不变的！ 例如，我母亲的名字对于循环是不变的！