Difference in loop invariant in for loop compared to while loop

Question

The invariant used for this example comes from https://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

I'm confused though. The code in the example uses a for loop.

I translated it to a while loop, because I understand this better, and I added assertions to test the invariant.

The while example makes total sense to me, and I can see how the invariant holds at each of the assertion points.

However, in the for example, the assertion assert total == sum(A[0:i]) and i >= len(A) fails.

I can see why it might for the i value, as i stops incrementing at 4. But I'm not sure why the final assertion for the sum needs to be assert total == sum(A[0:i + 1]).

It seems like quite a subtle thing going on here, around "off by one errors." I'm also a bit uncomfortable about the "hard-coding" of the invariant in assert total == sum(A[0:0])

Can anyone please provide an exact conversion of the while version of my code to a for version, with all the neccessary assersions for the invariant, and an explanation of how/why they are different?

Any help much appreciated.

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 Loop Variant

In your while loop i+=1 adds 1 to i and then checks the condition for while loop to continue or break. In given example condition is while i < 4. So at last when i becomes 5 while loop breaks and you get i=5.
So when you use it in slice it becomes [0:5] which will return element from index 0-4.

For Loop Variant

Compare this to for loop variant for loop will only iterate i from 0 to 4 and it will stop. Hence, value of i is 4 once for loop breaks.
So when you use it in slice it becomes [0:4] which will return element from index 0-3. Which in any case is not equal to total.

Final Analysis

• while breaks when i>4 and hence i becomes 5 and it breaks.
• for loop will iterate only from 0 to 4 and will break at 4.
• Hence value of i is different at the end of while and for loop.

Changes to get same behaviour for both the loop

• You need to add i+1 outside for loop variant to get same as while.
• And vice versa if you want while loop to act like for loop check for condition with i==len(A) which will break the loop at i=4 itself.