Introduction to Algorithms by Thomas H. Cormen, Charles E. Leiserson and Ronald L. Rivest and Clifford Stein : Chapter 2

The author provides a pseudocode implementation of insertion sort and defines loop invariant to provide a proof of the algorithm. Three properties of the loop invariant, Initialization, Maintenance and Termination are then proved by the author. The author then analyzes the time complexity of insertion sort and finds the best and worst case execution time of insertion sort in terms of input. The author then explains that the insertion sort algorithm is an iterative approach of problem solving and explains another approach divide and conquer to create another sorting algorithm mergesort. The author provides two implementation, recursive and non-recursive, for mergesort. The author also proves that merge sort takes $O(n \times \log n)$ time.