地精排序
类似于冒泡排序，从a[0]开始相邻元素之间两两进行比较，如果顺序则已排序序列长度i加1；如果这两个元素逆序，则i减1，向前冒泡（交换），直到不发生交换操作的位置。从该位置重复上述的操作，直至已排序序列长度i等于数组长度。（验证时间约5sec）
[Back to Index]
验证特点：量化断言，自定义谓词，蕴含式
标注说明：函数前条件：要排序数组的一般性质：长度和偏移；
函数后条件：排序后的数组a 的有序性描述。
程序样例 
类似于冒泡排序，从a[0]开始相邻元素之间两两进行比较，如果顺序则已排序序列长度i加1；如果这两个元素逆序，则i减1，向前冒泡（交换），直到不发生交换操作的位置。从该位置重复上述的操作，直至已排序序列长度i等于数组长度。（验证时间约5sec）
验证特点：量化断言，自定义谓词，蕴含式
标注说明：函数前条件：要排序数组的一般性质：长度和偏移；
函数后条件：排序后的数组a 的有序性描述。
程序样例