TITLE: The value of loop variable at the end of a loop in the insertion sort
QUESTION [0 upvotes]: I am looking at the algorithm of the insertion sort:
Input: $A[1 \dots n]$
 for j <- 2 to n
    key <- A[j]
    i <- j-1
    while (i>0 and A[i]>key)
          A[i+1] <- A[i]
          i <- i-1
    end
    A[i+1] <- key
 end

There is the following sentence:
$$\text{At the beginning of each iteration "for" ,the subsequence } A[1 \dots j-1] \\ \text{ consists of the elements that are from the beginning at these positions,  }\\ \text{ but sorted with the desired way.}$$
The proof of this sentence is the following:


Initial control, when $j=2:$ The sentence is true,because the subsequence  $A[1]$ \text{ is sorted in a trivial way 
Preservation control:  The algorithm moves the elements $ A[j-1], A[j-2], \dots $  to the right side,till the right position for $ A[j] $ is found. 
Verification of the result:  When the loop "for" ends, $j$ has the value $n+1$. The subsequence is now $ A[1 \dots n]$,  which is now sorted. 


Could you explain me why $j$ has the value $n+1$, when the loop "for" ends?
Can $j$ take the value $n+1$, although at the algorithm it is: for $j\leftarrow 2$ to $n$?

REPLY [2 votes]: The for loop is equivalent to a while loop:
for j <- 2 to n
    <stuff>
end

is equivalent to 
j = 2
while j <= n
    <stuff>
    j <- j+1
end

On the last pass through the loop, on entering the loop body, j will have the value n.  It will be incremented to n+1 at the bottom of the loop body and then the comparison will fail causing control to exit the loop.  Thus, immediately after the loop, the value of j is n+1.
{"set_name": "stack_exchange", "score": 0, "question_id": 860137}