LoopInvariant.md (715B)
1 # Loop Invariant 2 3 CLRS 2.1 4 5 **Definition:** A loop invariant is a condition that is true before and after a loop is ran. 6 7 In the case of insertion sort the loop invariant is that [0 : p] is sorted where p is the number of prior iterations (prior elements sorted). See [InsertionSort](InsertionSort.md) to understand this better. 8 9 Given that this must be true before and after running, we know it must be initialized as true which can sometimes mean manual running to get it started outside the loop itself to ensure proper iteration. 10 11 We call it maintenance when we are looping and making changes to ensure the invariance remains true. 12 13 Termaination is then the end of the loop whereby some condition has been met.