Proofs: Shell sort
These are the human proofs of Shell sort, at full length.
Shell sort sorts the array and keeps its items full
This proof shows: correctness.
For a gap , the chain of a residue with is the list of the items at the indices that are less than . The array is -sorted when each chain is sorted.
Lemma (one pass). One step of the loop of line L1, with the gap , permutes the items of each chain among the indices of that chain, and after it the array is -sorted.
Proof. Lines L3 to L8 only read and write the indices , which are all in the chain of . So the pass works on each chain apart from the others, and it does not move an item to another chain. For one chain, list its indices as . The step of line L2 for is the step of insertion sort for position of this chain: line L5 compares with , line L6 shifts each larger item one place up in the chain, and line L8 writes the key into the gap that is left. We use this invariant, before the step for :
The items at are the items that were there at the start of the pass, in sorted order.
It holds for , because one item is sorted. Assume it before the step for . The loop of line L5 stops at the first index , going down from , with or . Each of is larger than , and each moves one place up in the chain. Then line L8 puts at . The items at are at most and sorted, the items at are larger than and sorted, so hold the old items plus in sorted order. The steps for indices in other chains do not touch this chain. At the end of the pass, , so each chain is sorted. The step for each ends because falls by in each turn of line L5 and the loop stops at .
Theorem. If is a finite list of positive gaps whose last gap is , then SHELL-SORT stops, and after it holds the same items, in non-decreasing order.
Proof. Each line moves items only by the shift of line L6 and the write of line L8, and by the lemma each pass permutes the items of each chain. So the multiset of the items does not change. There are finitely many passes, and each pass has steps that each end, so the algorithm stops. The last pass has . With there is one chain, the full array, so by the lemma the array is sorted after this pass.
The earlier passes are not needed for correctness. They only make the last pass fast, because they remove most of the inversions before it.