插入排序
插入排序将数组a的第一个元素a[0]设定为初始有序数组段，然后从a[1]开始将数组的其余元素逐个插入到该有序数组段中。
插入过程是从有序数组段的后面将要插入的元素a[i]与数组段a[0..i-1]中的元素逐个比较，直至插入合适的位置，即 a[j-1] <= a[i] < a[j+1]。（验证时间约 16sec）
[Back to Index]
验证特点：量化断言，循环变式
标注说明：函数前条件：函数入口处数组的一般性质；
函数后条件：排序后的数组a 的有序性描述。
程序样例 
