思想是直接插入排序，即每次拿一個數字向已排序好的數字中插入，採用迴圈不變式的設計思想。

  迴圈不變式：一般而言,用這個式子表示希望得到的結果,如果在迴圈的每一步,這個式子都是正確的,那麼迴圈結束後,這個式子也正確,並得到了期望的結果。

 如何證明迴圈的每一步式子都是正確的？

 需要證明式子滿足三個性質：

 初始化：迴圈的第一次迭代之前，它為真。

 保持：如果迴圈的某次迭代之前它為真，那麼下次迭代仍然為真。

 終止：證明迴圈終止時，是期望結果。

程式碼：

package com.zjq.arithmetic.sort;

public class Insert_Sort {

	public static void main(String[] args) {
		int[] eg={3,2,4,5,1,6};
		Insert_Sort insert_Sort=new Insert_Sort();
		eg=eg=insert_Sort.insertSort(eg);
		for(int m=0;m<eg.length;m++){
			System.out.println(eg[m]);
		}
	}
	/**迴圈不變式
	 * @param array
	 * @return
	 */
	public int[] insertSort(int[] array){	
		for(int i=1;i<array.length;i++){
			int k=array[i];
			int j=i-1;
			while(j>=0&&array[j]>k){
				array[j+1]=array[j];
				j=j-1;
			}
			array[j+1]=k;
		}
		return array;
	}

}
 

此程式碼滿足迴圈不變的三個性質。

1 初始化：迴圈下標從1開始，初始時候下標0,陣列只有一個數array[0],當然是排序好的。

2 保持:每次迴圈是將新的數字插入到上一次排序好的陣列中，得到讓然是排序好的陣列。

3 終止;迴圈終止時候，得到的是原陣列排序好的陣列，符合期望。