public static void insertionSort(int[] to_sort) {

    // Precondition: Array to_sort contains a multiset of ints
	
    int n = to_sort.length;
    int i = 1;

    while(i < n) { // Loop-1

        // Loop-1 invariants:
        // 1) 
	//
	// 2)
	//

	int val = to_sort[i];
	int j = i - 1;

	while(j >= 0 && val < to_sort[j]) { // Loop-2

	    // Loop-2 invariants:
	    // 1) If val were stored in to_sort[j+1], to_sort would contain
	    //    all of the original data
	    // 2) Ignoring to_sort[j+1], the subarray to_sort[0...i] is
	    //    sorted
	    // 3) All of the data in the subarray to_sort[j+2...i] is
	    //    greater than or equal to val

	    to_sort[j + 1] = to_sort[j];

	    // Assertions:
	    //
	    //
	    //

	    j--;

	    // Assertions:
	    //
	    //
	    //

        }

	// Loop-2 postcondition: If val were stored in to_sort[j+1], the 
	// subarray to_sort[0...i] would be sorted and would contain all
	// of the original data

	to_sort[j+1] = val;
	i++;

    }

    // Loop-1 postconditions:
    // 1) 
    //
    // 2)
    //

}