Correctness with loop invariants

Analysis covers correctness as well as speed: an algorithm that is fast but wrong is useless. A loop invariant is a statement about the program state that is true before every iteration of a loop. Proving correctness with an invariant has three parts: initialization (it is true before the first iteration), maintenance (if it is true before an iteration, it stays true after), and termination (when the loop ends, the invariant gives a useful property).

def insertion_sort(values):
    items = list(values)
    for i in range(1, len(items)):
        assert items[:i] == sorted(items[:i])
        key = items[i]
        j = i - 1
        while j >= 0 and items[j] > key:
            items[j + 1] = items[j]
            j -= 1
        items[j + 1] = key
    assert items == sorted(items)
    return items


print(insertion_sort([5, 2, 4, 6, 1, 3]))
print(insertion_sort([]))