* Suppose $P$ holds for some `0 ≤ i < n - 1`. Then `A[0..i-1]` is a sorted array of the `i` least elements of `A`. Our inner loop then finds the smallest element in `A[i..n]` and swaps it with `A[i]`. Therefore `A[0..i]` is a sorted array of the `i + 1` least elements of `A`. At the end of the iteration, `i` is incremented meaning `A[0..i-1]` still satisfies $P$.
* On termination, `i = n - 1` and `A[0..n-2]` are the `n - 1` least elements of `A` in sorted order. But, by exhaustion, `A[n-1]` must be the largest element meaning `A[0..n-1]`, the entire array, is in sorted order.
%%ANKI
Basic
Given array `A[0..n-1]`, what is selection sort's loop invariant?
Back: `A[0..i-1]` is a sorted array of the `i` least elements of `A`.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707398773331-->
END%%
%%ANKI
Basic
What is initialization of selection sort's loop invariant?
Back: Sorting starts with an empty array which is trivially sorted.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707398773333-->
END%%
%%ANKI
Basic
What is maintenance of selection sort's loop invariant?
Back: Each iteration puts the next least element into the sorted subarray.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707398773334-->
END%%
%%ANKI
Basic
How does selection sort partition its input array?
Back:
```
[ sorted | unsorted ]
```
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707399790952-->
END%%
%%ANKI
Basic
Which element will selection sort move to `sorted`?
```
[ sorted | unsorted ]
```
Back: The least element in `unsorted`.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).