Loop invariant when first iteration starts

Question

I'm taking an elementary course in data structures & algorithms, the book we use is the seminal work by CLRS. I have some trouble understanding the loop invariant as explained in chapter 2.1: Insertion Sort.

The book says that:

At the start of each iteration of the for loop of lines 1-8, the subarry A[1..j -1] consists of the elements originally in A[1..j-1], but in sorted order.

Now, this puzzles me. Why does this hold when the first iteration starts? Say the array to be sorted looks like { 5, 2, 4, 6, 1, 3 }. Now when the first iteration of the for loop starts A[1.. j-1] isn't in sorted order, when the iteration ends it is though.

What am I missing here?

Answer 1

A[1.. j-1] isn't in sorted order, when the iteration ends it is though.

Assuming the value of j starts at 2 initially, A[1.. j-1] will only contain an array of length 1, which by definition is sorted.