排序算法之：循环不变式在二分插入排序中的正确性证明 题目描述：使用循环不变式证明二分插入排序算法的正确性。二分插入排序是插入排序的优化版本，通过二分查找确定插入位置，减少比较次数但保持O(n²)时间复杂度。 解题过程： 算法步骤回顾 从第二个元素开始遍历数组（i=1到n-1） 对每个元素arr[ i]，使用二分查找在已排序子数组arr[ 0...i-1 ]中找到插入位置 将arr[ i ]插入到正确位置，已排序部分向右移动元素 定义循环不变式 在每次迭代开始时（i=k），子数组arr[ 0...k-1 ]始终保持有序 这个有序子数组包含原始数组中前k个元素的排序版本 初始化证明（第一次迭代前） 当i=1时，子数组arr[ 0...0 ]只有一个元素 单元素数组自然是有序的，满足循环不变式 保持证明（每次迭代保持性质） a) 二分查找正确性： 在有序子数组arr[ 0...i-1 ]中执行二分查找 查找过程维护左右指针，确保插入位置左侧元素≤目标值，右侧元素≥目标值 b) 插入操作正确性： 找到位置pos后，将arr[ pos...i-1 ]的元素右移一位 将原arr[ i]插入到arr[ pos ]位置 新子数组arr[ 0...i ]保持有序，因为： arr[ 0...pos-1 ]保持有序且≤新元素 arr[ pos ]是新插入的元素 arr[ pos+1...i]是原arr[ pos...i-1 ]（都≥新元素）且保持有序 终止证明（算法结束时） 当i=n时循环结束，此时arr[ 0...n-1 ]已排序 整个数组有序，算法正确 边界情况验证 空数组：循环不执行，自然有序 单元素数组：直接返回，正确 重复元素：二分查找找到第一个≥目标值的位置，保持稳定排序特性 通过这个循环不变式证明，我们严格证明了二分插入排序的正确性，确保算法在任何输入情况下都能产生正确的排序结果。