归并排序
归并排序（Merge Sort）是建立在归并操作上的一种有效的排序算法，是分治法（Divide and Conquer）的一个典型的应用。
算法的基本思想是将数组a[0..n-1]分为2部分：a[0..n/2]和 a[n/2+1..n-1] 分别进行排序，然后再将2个有序子序列合并为有序序列。
每个子序列也都采用归并排序，先自顶向下对子序列进行逐级分割直至子序列不多于2个元素。然后再自底向上进行合并，完成整个数组的排序。（验证时间约 95sec）
[Back to Index]
验证特点：自定义谓词，蕴含式，量化断言，递归，终止性描述
标注说明：本文件有三个函数，分别是有序数组段的归并 merge、数组段的排序 msort和数组的排序 mergesort。
函数的前后条件请见程序中各函数的描述。
程序样例 
