how i can find the loop invariant and prove correctness?

i am learning correctness and struggling to find the appropriate loop invariant and prove its correctness.

I think the loop invariant should be the t=sum of the positive value but i don't know how to write it correctly or is there any other loop invariant?

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

Before getting formal, it is sometimes helpful to think in terms of "what stays the same" and "what changes" as regards the loop.* For the loop written, we have these variables of interest:

• A - the array of numbers to sum
• n - the integral number of elements in A.
• t - as written, I assume intended to be the eventual sum-of-positives
• i - the index variable; sometimes called the variant

So what changes each iteration? The array A does not change. The number of elements n in the array does not change. As written, the sum t might change. The index variable i will change.

As pertains to the loop, then, folks generally say that i is the variant. It increments every iteration and a comparison of it against n is what exits the loop.

The invariant of interest to me is that t will always represent the calculated-so-far sum-of-positives. For example, on the first iteration:

• Before the iteration, i == 0 and t is also correctly 0
• After the iteration, i == 1 and t will be correct with respect to the first element.

However, as written, the return statement precludes any processing beyond the first element of the array. Moving from theory to practice, how then might you fix the implementation?

* For the pedantic, the qualifier is important because strictly speaking an "invariant" is something that does not vary -- does not change, or always holds true -- for every iteration of the loop. So? Lots of statements are invariant with respect to the loop! For example, my mother's name is invariant for the loop!