排序算法之：循环不变式在珠排序（Bead Sort）中的正确性证明 题目描述 珠排序（Bead Sort）是一种自然排序算法，它通过模拟重力作用下珠子在竖杆上掉落的过程来对非负整数序列进行排序。假设有n个数字，每个数字表示该位置竖杆上的珠子数量。排序时，珠子逐行向下掉落，最终每列的珠子数会按非递增顺序排列。请使用循环不变式方法严格证明珠排序的正确性，包括其排序结果的有序性和稳定性（若适用）。 解题过程 理解珠排序的基本操作 假设输入数组为 A[0..n-1] ，元素为非负整数，表示每根竖杆的初始珠子数。 算法步骤： 找出最大值 max ，确定需要的"行数"（即最大珠子数）。 初始化一个二维网格（ max 行× n 列），初始时每列从上到下放置 A[i] 个珠子（1表示有珠子，0表示无）。 模拟重力：所有珠子同步向下掉落，直到每行的珠子连续靠左排列。 从网格中读取每列的珠子数，得到排序后的数组。 定义循环不变式 我们将排序过程分解为行处理循环（从上到下逐行处理珠子掉落）。对于第 k 次迭代（处理第 k 行），循环不变式为： "前 k 行中，每行的珠子数量是该行在所有行中的最终数量，且每行珠子从左向右连续排列（无间隔）。" 初始状态（k=0） 尚未处理任何行，网格保持初始状态。 循环不变式自然成立（前0行满足条件）。 保持状态（k → k+1） 假设前 k 行已满足不变式：每行珠子数固定且连续靠左。 处理第 k+1 行时： 该行珠子受重力掉落，会填充到下方最近的空位，但 不会改变上方已处理行的结构 （因为重力方向向下）。 掉落完成后，第 k+1 行的珠子数等于原始网格中第 k+1 行及以下所有行在该行的珠子数之和，且因重力作用紧密左对齐。 因此，前 k+1 行仍满足不变式。 终止条件 当 k = max 时，所有行处理完毕。 根据不变式，所有行均满足珠子连续左对齐，此时每列的珠子数即为排序后的结果。 由于每行珠子数固定，且排列连续，最终每列的珠子数必然呈非递增顺序（左多右少）。 正确性结论 有序性 ：终止时，每列珠子数从左到右非递增，即数组降序排列。若需升序，反转结果即可。 稳定性 ：珠排序对非负整数稳定，因为原始数据中相同值的珠子在掉落前后相对水平位置不变（重力仅垂直作用）。 通过以上循环不变式，我们严格证明了珠排序的输出必然有序，且保持了相同元素的原始相对顺序。