快速排序
快速排序由C. A. R. Hoare在1960年提出。它的基本思想是：
先将要排序的数据列分割成独立的两部分，使得其中一部分的所有数据都比另外一部分的所有数据都要小，然后再分别对这两部分数据进行快速排序。
整个排序过程递归进行，重复上述过程直至分区小于等于2个元素，以此达到整个数据列成为有序序列。（验证时间约为740sec）
[Back to Index]
验证特点：归纳谓词，类型不变式，数组的置换性，幽灵变量，幽灵形参，多命名行为
标注说明：利用函数的幽灵形参标记数组的分段有序性。
本例主要有2个函数，分别是数组段的划分（partition）和排序（quick_sort）。测试用函数（gosorting）启动排序。各函数协议请见程序中的说明。
程序样例 
