Overview
Property | Value |
---|---|
Best Case | |
Worst Case | |
Avg. Case | |
Aux. Memory | |
Stable | Yes |
Adaptive | Yes |
Loop Invariant
Consider loop invariant given by
A[0:i-1]
consists of the originalA[0:i-1]
elements but in sorted order.
We prove maintains the requisite properties:
- Initialization
- When
i = 1
,A[0:0]
contains a single element. This trivially satisfies .
- When
- Maintenance
- Suppose holds for some
1 ≤ i < n
. ThenA[0:i-1]
consists of the originalA[0:i-1]
elements but in sorted order. On iterationi + 1
, the nested for loop putsA[0:i]
in sorted order. At the end of the iteration,i
is incremented meaningA[0:i-1]
still satisfies .
- Suppose holds for some
- Termination
- The loop ends because
i < n
is no longer true. Theni = n
. Since holds, this meansA[0:n-1]
, the entire array, is in sorted order.
- The loop ends because
Analogy
Suppose you have a shuffled deck of playing cards face-down on a table. Start by grabbing a card from the deck with your left hand. For the remainder of the cards, use your right hand to transition the topmost card to the end of your left hand. If the newly placed card isn’t in sorted order, move it one position closer to the start. Repeat until it’s in sorted order.
If you repeat this process for every card in the deck, your left hand will eventually contain the entire deck in sorted order.
Bibliography
- Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022).