for 循环与 while 循环中循环不变性的差异

Question

此示例使用的不变量来自https://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

我很困惑。示例中的代码使用循环for。

我将其翻译为while循环，因为我更好地理解这一点，并且添加了断言来测试不变量。

这个while例子对我来说完全有意义，我可以看到不变量在每个断言点上是如何成立的。

然而，在该for示例中，断言assert total == sum(A[0:i]) and i >= len(A)失败。

我可以理解为什么它可能会影响该i值，因为i在 处停止递增4。但我不确定为什么总和的最终断言需要是assert total == sum(A[0:i + 1])。

这似乎是一件非常微妙的事情，围绕着“差一个错误”。我对不变量的“硬编码”也有点不舒服assert total == sum(A[0:0])

while任何人都可以提供我的代码版本到版本的精确转换for，以及不变量的所有必要断言，并解释它们如何/为什么不同？

非常感谢任何帮助。

def my_sum_while(A):
    """
    Loop Invariant: At the start of iteration i of the loop, the variable
    `total` should contain the sum of the numbers from the subarray A[0:i].
    """
    i = 0
    total = 0
    assert total == sum(A[0:i])
    while i < len(A):
        assert total == sum(A[0:i])
        total += A[i]
        i += 1
    assert total == sum(A[0:i]) and i >= len(A)
    return total
    
xs = [1, 2, 3, 4, 5]
print(my_sum_while(xs))

def my_sum_for(A):
    """
    Loop Invariant: At the start of iteration i of the loop, the variable
    `total` should contain the sum of the numbers from the subarray A[0:i].
    """
    total = 0
    assert total == sum(A[0:0])
    for i in range(len(A)):
        assert total == sum(A[0:i])
        total += A[i]
    assert total == sum(A[0:i]) and i >= len(A)
    return total
    
xs = [1, 2, 3, 4, 5]
print(my_sum_for(xs))

Answer 1

While 循环变体

在 while 循环中添加i+=1然后检查循环继续或中断的条件。在给定的示例中，条件是。所以最后当成为循环中断时，你得到了。 因此，当您在切片中使用它时，它将从索引返回元素。1iwhilewhile i < 4i5 whilei=5
[0:5]0-4

For 循环变体

for与循环变体相比，for循环只会迭代i并且0 to 4会停止。因此， 的值i是4循环中断一次。
因此，当您在切片中使用它时，它将[0:4]从索引返回元素0-3。无论如何都不等于total。

最终分析

• while当它变成时就会破裂i>4，因此它就破裂了。i5
• for循环将仅从 迭代0 to 4并在 处中断4。
• 因此，在and循环i结束时，的值是不同的。whilefor

进行更改以使两个循环获得相同的行为

• 您需要添加i+1外部for循环变体才能获得与while.
• 反之亦然，如果您希望while循环像for循环一样检查条件，i==len(A)从而打破循环i=4本身。