insertion sort is an algorithm that solves the sorting problem.

## constituents

a sequence of \(n\) numbers \(\{a_1, \dots a_{n}\}\), called keys

## requirements

Insertion sort provides an ordered sequence \(\{a_1’, \dots a_{n}’\}\) s.t. \(a_1’ \leq \dots \leq a_{n}’\)

## implementation

I don’t know why, but it seems like CLRS’ implementation is back-to font. But perhaps I’m just mistaken.

```
void insertion_sort(int length, int *A) {
for (int j=1; j<length; j++) {
int key = A[j];
// insert the key correctly into the
// sorted sequence, when appropriate
int i = j-1;
while (i > 0 && A[i] > key) { // if things before had
// larger key
// move them
A[i+1] = A[i]; // move it down
// move our current value down
i -= 1;
}
// put our new element into the correct palace
A[i+1] = key;
}
}
```

## additional information

### proof

We use loop invariant method to show that our algorithm is correct. Our invariant is that the array \(A[0, \dots, j-1]\) is sorted \(\forall j 0 \dots L+1\).

- Initialization: at the first step, \(j=1\) (second element), the subarray of \(A[0, \dots j-1]\) (namely, only the first element), is sorted trivially
- Maintenance: during each loop, we move \(j\) to the right, only being done when the subarray to the left is correctly sorted
- because of \(j\) is moving forward until length, it will terminate

As \(j\), by the end, covers the entire loop, our loop terminates at \(L+1\) and invariant (sortedness) is maintained between \(A[0, \dots j]\).