Some more about Loop Invariant:
A loop invariant is some condition that holds for every iteration of the loop.
Three properties of the loop invariant-
1) Initialization- It is true prior to the 1st iteration of the loop.
2) Maintenance - If it is true before an iteration of the loop, it remains true before the next iteration.
and
The most important one-
3)Termination- When the loop terminates, this property, along with termination conditions, helps to show that the algorithm is correct.
See Code below-
int j = 9;
for(int i=0; i<10; i++)
j--;
Here at any iteration "i+j ==9" this predicate (condition) always holds, So it is loop invariant.
After the loop terminates i=10 and j=-1 i+j=10+(-1)=9.
Now consider Insertion Sort. In this sorting, we have an array[1..n] we know at any iteration i ,Array elements from 1 to i-1 always sorted and at the end we get array elements from 1 to n in sorted order. So, loop invariant is A[1...i-1] sorted.
When we write any algorithm, our goal is to maintain loop invariants.
Consider Insertion sort again.
Step 1: initialize loop invariant: A[1] is sorted.
Step 2: Maintain loop invariant (A[1 to i-1] should be sorted for any i)
Step 3: After termination of the loop-
Once we get out of loop, we achieve our Goal (Sorting) If we maintain loop invariant.
loop terminates when i=n+1.
A[1...i-1]=A[1...n+1-1]=A[1...n]. So we get the sorted array at the end.
Here in this question, each time we are taking out Least significant digit of n, and appending it to rev.
Here for any i, what will be true for $n$ and $\text{rev}$ ?
$n=d_1\, d_2 \,\ldots\, d_{m-i} \qquad \mathbf{and} \qquad \text{rev} = d_m\,d_{m-1} \,\ldots\, d_{m-i+1}$