排序算法之：循环不变式在二分插入排序中的正确性证明 题目描述： 使用循环不变式证明二分插入排序算法的正确性。二分插入排序是插入排序的优化版本，在寻找插入位置时使用二分查找代替线性查找，但插入操作仍需要移动元素。需要证明该算法确实能正确地将数组排序。 解题过程： 算法回顾 首先明确二分插入排序的步骤： 从第二个元素开始（索引1），将每个新元素插入到前面已排序的子数组中 对于当前元素arr[ i]，使用二分查找在arr[ 0...i-1 ]中找到合适的插入位置 将arr[ i ]插入到正确位置，需要移动插入位置后的所有元素 定义循环不变式 循环不变式是证明算法正确性的关键工具。对于二分插入排序，我们定义： "在每次外层循环迭代开始时（处理第i个元素），子数组arr[ 0...i-1 ]已经按升序排列" 证明循环不变式的三个性质 性质1：初始化 当i=1时，子数组arr[ 0...0 ]只包含一个元素 单元素数组自然是有序的 因此循环不变式在第一次迭代前成立 性质2：保持 假设在第i次迭代开始时，arr[ 0...i-1]已排序。我们需要证明经过第i次迭代后，arr[ 0...i ]仍然有序： 二分查找会在arr[ 0...i-1 ]中找到正确的插入位置pos 因为二分查找在有序数组上工作，所以找到的位置保证arr[ 0...pos-1] ≤ arr[ i] ≤ arr[ pos...i-1 ] 将arr[ i]插入位置pos后，新数组arr[ 0...i ]保持有序 因此循环不变式在迭代过程中保持不变 性质3：终止 当循环结束时，i = n（数组长度） 根据循环不变式，此时arr[ 0...n-1 ]已经排序 这正是算法期望的最终结果 二分查找的正确性证明 需要单独证明二分查找在有序子数组中的正确性： 二分查找的循环不变式："搜索范围[ low, high ]始终包含正确的插入位置" 通过维护low和high指针，每次比较后将搜索范围减半 最终low > high时，low就是正确的插入位置 移动操作的正确性 插入操作需要将arr[ pos...i-1 ]的元素向右移动一位 这个操作保持了元素的相对顺序 移动后在位置pos放入arr[ i ]，整个数组保持有序 结论 通过循环不变式的三个性质都得到满足，可以证明二分插入排序算法是正确的。二分查找的引入优化了比较次数（从O(n²)降到O(n log n)），但移动操作的时间复杂度仍然是O(n²)。