understanding loop invariants I have a bit of experience with loop invariants but I'm not really clear on them. I'm trying to learn them through an Algorithm I have.
Reverse(X,Y)
   n = X.length 
   for(i = 1 to n)
      Y[n - i + 1] = X[i] 
   return Y

This copies values in array X into array Y in reverse order, and returns array Y. If X and Y both have length n (i.e., n = X.length = Y.length) and both arrays are indexed from 1 to the length of the array, what would be some loop invariants for the for loop which would prove its correctness?
The reverse of X[:i], the prefix of X up to the $i$-th position is equal to Y[n-i+1:], the suffix of Y from the $(n-i+1)$-th position onward.
Before the loop starts, which we could consider as $i=0$, we have that the reverse of the prefix of X of length zero is equal to suffix of Y of length zero.
Each step of the loop preserves the property for the previous value of i and makes the property true for the current value of i.
At the end of the loop the property is satisfied for i=n, which implies that the reverse of X is equal to Y.