排序算法之：循环不变式在选择排序中的正确性证明 题目描述： 使用循环不变式（Loop Invariant）来严格证明选择排序（Selection Sort）算法的正确性。选择排序的基本思想是反复从未排序部分选择最小元素放到已排序部分的末尾。我们需要通过定义和维护循环不变式，证明算法在每次迭代后都能保持某种正确状态，最终完成排序。 解题过程： 选择排序算法回顾 算法步骤： 从数组第一个元素开始，将整个数组视为未排序部分 在未排序部分中找到最小元素 将该最小元素与未排序部分的第一个元素交换 将未排序部分的边界向右移动一个位置 示例：对 [ 5, 2, 4, 6, 1, 3 ] 排序 第1轮：找到最小值1，与5交换 → [ 1, 2, 4, 6, 5, 3 ] 第2轮：在子数组[ 2,4,6,5,3]中找到最小值2，已在正确位置 → [ 1, 2, 4, 6, 5, 3 ] 继续这个过程直到完全排序 定义循环不变式 令A[ 0..n-1 ]为待排序数组 定义循环不变式：在算法第i次迭代开始时（i从0开始计数），子数组A[ 0..i-1 ]包含原数组中已排序的i个最小元素，且这些元素已处于最终正确位置 具体来说： 初始化：当i=0时，A[ 0..-1 ]为空数组，包含0个最小元素（平凡正确） 保持：如果第i次迭代前不变式成立，那么经过找到第i小的元素并交换后，A[ 0..i ]将包含已排序的i+1个最小元素 终止：当i=n时，A[ 0..n-1 ]包含所有n个已排序元素 初始化证明（Initialization） 在循环开始前（i=0），已排序部分为空数组 空数组自然包含0个最小元素，且是有序的 因此循环不变式在第一次迭代前成立 保持证明（Maintenance） 假设在第i次迭代开始时，A[ 0..i-1 ]包含已排序的i个最小元素 在第i次迭代中： a. 在未排序部分A[ i..n-1]中找到最小元素A[ min_ index ] b. 将A[ i]与A[ min_ index ]交换 交换后： A[ i ]现在是未排序部分中的最小元素，也是整个数组中第i+1小的元素 A[ 0..i ]现在包含已排序的i+1个最小元素 由于我们只交换了A[ i]和A[ min_ index]，A[ 0..i-1 ]保持不变 因此循环不变式在迭代后仍然保持 终止证明（Termination） 当i=n时循环结束 根据循环不变式，A[ 0..n-1 ]包含已排序的所有n个元素 由于数组有n个元素，这意味着整个数组已经完全排序 边界情况分析 空数组：循环不执行，直接返回空数组（正确） 单元素数组：i从0到n-1，但实际只执行一次查找最小值和交换（元素与自身交换），结果正确 已排序数组：每次找到的最小值就是当前未排序部分的第一个元素，仍然正确工作 算法正确性结论 通过循环不变式的三个步骤（初始化、保持、终止）的严格证明 我们证明了选择排序算法能够正确地将任意数组排序 这种证明方法确保了算法的逻辑正确性，而不仅仅是基于测试用例的验证 这个证明展示了循环不变式作为形式化验证工具的强大之处，它为我们提供了严格证明算法正确性的数学框架。