The value of loop variable at the end of a loop in the insertion sort

Question

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$?

Answer 1

Some languages have for loops that do this. It goes through the content of the for loop, then it updates j, then it checks j. So if we go through the loop for j=n, it will update j to be n+1 and THEN check if we want to use j if it's between 2 and n. So it decides it's not and exits. But it already incremented j. That is only if you aren't getting any unusual behavior or faults.

So, if it's not performing incorrectly and it's just j being n+1, then it's harmless and part of the nature of the for loop. However, this may not be the issue if you're getting an error or wrong sorting.

Answer 2

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.