希尔（Shell）排序
希尔排序是一种分组的插入排序。
它将数组a 按增量分组，对每组使用直接插入排序算法排序。增量从n/2开始逐次递减，直至增量减至为1，完成排序。（验证时间约 28sec）
[Back to Index]
验证特点：量化断言，循环嵌套、循环不变式、循环变式和幽灵语句
标注说明：函数前条件：函数入口处数组的一般性质，即数组的大小；
函数后条件：排序后的数组a 的有序性描述。
程序样例 
希尔排序是一种分组的插入排序。
它将数组a 按增量分组，对每组使用直接插入排序算法排序。增量从n/2开始逐次递减，直至增量减至为1，完成排序。（验证时间约 28sec）
验证特点：量化断言，循环嵌套、循环不变式、循环变式和幽灵语句
标注说明：函数前条件：函数入口处数组的一般性质，即数组的大小；
函数后条件：排序后的数组a 的有序性描述。
程序样例