排序算法之：循环不变式在堆排序中的正确性证明 题目描述： 堆排序是一种高效的比较排序算法，它利用堆这种数据结构的特性进行排序。我们需要使用循环不变式的方法来严格证明堆排序的正确性，包括建堆过程和排序过程。 解题过程： 堆排序算法回顾 堆排序分为两个主要阶段： 建堆阶段：将无序数组构建成最大堆（或最小堆） 排序阶段：反复将堆顶元素（最大值）与堆末尾元素交换，然后调整堆 循环不变式的定义 对于建堆阶段，我们定义循环不变式： "对于从最后一个非叶子节点开始到当前节点i的所有子树，都满足堆的性质（父节点大于等于子节点）" 建堆阶段的正确性证明 步骤1：初始化 从最后一个非叶子节点开始（索引为n/2-1） 此时，所有叶子节点都是单节点的堆，满足堆性质 循环不变式在初始化时成立 步骤2：保持 假设在处理节点i时，i的所有子树都已经满足堆性质 对节点i执行堆化操作（heapify） 堆化操作确保以i为根的子树满足堆性质 处理完节点i后，循环不变式保持成立 步骤3：终止 当处理到根节点（索引0）时 整个数组满足堆性质，建堆完成 循环不变式证明整个堆构建正确 排序阶段的循环不变式 定义排序阶段的循环不变式： "在每次迭代中，数组分为三个部分： A[ 0...i ]：当前堆的有效部分（满足堆性质） A[ i+1...n-1 ]：已排序部分（升序排列，且都大于等于堆中元素） A[ i+1...n-1]中的元素都大于等于A[ 0...i ]中的元素" 排序阶段的正确性证明 步骤1：初始化 i = n-1，整个数组是一个最大堆 已排序部分为空，循环不变式成立 步骤2：保持 将堆顶元素A[ 0]（最大值）与A[ i ]交换 此时A[ i]是当前最大值，已排序部分A[ i...n-1 ]保持升序 对A[ 0...i-1 ]执行堆化，恢复堆性质 循环不变式得到保持 步骤3：终止 当i = 0时，堆中只剩一个元素 整个数组按升序排列，排序完成 完整正确性证明 通过两个循环不变式的结合，我们证明了： 建堆过程正确地将无序数组构建成堆 排序过程正确地利用堆性质进行排序 最终得到的数组是完全有序的 这个证明确保了堆排序算法在任何输入情况下都能正确工作。