I am currently learning Loop Invariants and is wondering whether I have generated them correctly here. The algorithm pseudocode is:
**EvenSumming(A)**
outcome=0
for i=1 to n
if A[i] is even
outcome=outcome+A[i]
return outcome
So far my LI and proving:
Loop Invariant (LI): At every iteration, the variable outcome is always even and at most can only be composed of i-1 elements originally in A[i....n].
Initialization: Let i = 1, thus outcome starts at 0, which makes it an even number and is composed of 0 elements from A[1...n]
Maintenance: By math, we have that adding two even numbers always results in an even number, and since every iteration in the array increments i by 1 then trivially we know that there are i-1 elements that have been iterated through before i. Thus, at iteration i, outcome will be an even value composed of at most i-1 elements from A[i...n]
Termination: At termination, let i > n and thus we can say that i = n+1. Then by LI we have that outcome is still even value composed from at most n elements originally existing in A[n]