冒泡排序（可置换性）
排序算法的程序实现应保证排序后的数组与原数组具有完全相同的元素，即排序后的数组是原数组中数组元素的一个排列，也就是说排序后的数组是原数组的一个置换。
本例在验证冒泡排序函数正确性的基础上，增加了对数组置换性的证明。 （验证时间约 83sec）
[Back to Index]
验证特点：量化断言，自定义谓词，归纳谓词，幽灵变量，逻辑数组，引理
标注说明：函数前条件：给出排序前数组a的性质：长度和偏移，并用逻辑数组olda记录函数被调用时，在入口处数组a的值；
函数后条件：给出数组a的有序性（递增）描述，同时说明排序后的数组a是原数组olda的一个置换。
程序样例 
