循环不变式在冒泡排序中的正确性证明

题目描述
冒泡排序是一种简单的排序算法，它通过重复遍历数组，比较相邻元素并交换它们的位置，使较大的元素逐渐“浮”到数组末端。现在要求你使用循环不变式（Loop Invariant）来严格证明冒泡排序的正确性，确保算法执行后数组一定按升序排列。

解题过程
循环不变式是证明算法正确性的核心工具，它指在循环的每次迭代前后均保持为真的条件。对于冒泡排序，我们关注其外层循环的循环不变式。

1. 定义循环不变式
   冒泡排序的外层循环（假设从第 1 轮到第 n-1 轮）的循环不变式可表述为：
   “在第 i 轮迭代结束后，数组末尾的 i 个元素是全局最大的 i 个元素，并且它们已按升序排列。”
   例如，第 1 轮结束后，最后一个元素是最大值；第 2 轮结束后，最后两个元素是最大的两个且已排序，依此类推。

2. 初始状态（Initialization）
   在循环开始前（i=0），数组末尾的 0 个元素视为已排序。此时不变式自然成立，因为没有任何元素需要验证。

3. 保持状态（Maintenance）
   假设在第 i 轮迭代开始时，不变式对 i-1 成立（即末尾 i-1 个元素已排序且最大）。本轮中，内层循环会遍历未排序部分（前 n-i 个元素），通过相邻比较和交换，将未排序部分的最大值“冒泡”到位置 n-i（即未排序部分的末尾）。因此：

   • 第 n-i 位置的元素被固定为当前未排序部分的最大值；
   • 末尾的 i 个元素（包括新固定的元素）仍然是全局最大的 i 个元素，且保持升序。
     不变式在第 i 轮结束后依然成立。

4. 终止状态（Termination）
   当外层循环进行到 i=n-1 时，末尾 n-1 个元素已是全局最大的 n-1 个元素且已排序。此时剩余的第一个元素自然是最小值，整个数组按升序排列。循环不变式保证了最终结果的正确性。

5. 边界情况处理

   • 若数组已排序，内层循环无交换操作，算法提前终止（可优化）。
   • 若数组逆序，每轮均需完整比较，但不变式仍确保正确性。

通过以上三步（初始、保持、终止），循环不变式完整证明了冒泡排序的正确性。