首先明确：你实现的这个partition方法是Hoare快速排序分区的经典变体，和标准Hoare分区的核心逻辑一致（双向扫描、指针相向移动），只是把指针的初始调整（i递增、j递减）放到了外层循环体内，而非循环前。接下来我们修正并证明正确的循环不变量。

正确的循环不变量定义 #

针对partition方法中外层while i < j的每次迭代开始时，以下条件始终成立：
对于数组arr的任意索引k：

• arr[p] = y（y是初始选取的基准值，全程未被修改直到循环结束后的交换）
• 所有满足p < k <= i-1的k，都有arr[k] < y
• 所有满足j+1 <= k <= r的k，都有arr[k] > y
• 指针边界约束：i <= r+1，j >= p-1

循环不变量的证明 #

我们按照循环不变量证明的三个标准步骤：初始化、保持、终止来验证。

1. 初始化（第一次进入外层循环前） #

此时i = p，j = r+1，还未执行任何循环体操作：

• arr[p] = y：显然成立，因为我们一开始就将y赋值为arr[p]，且未修改该位置。
• p < k <= i-1即p < k <= p-1：不存在这样的索引k，该条件空真（vacuously true）。
• j+1 <= k <= r即r+2 <= k <= r：同样不存在这样的索引k，条件空真。
• 指针约束：i = p <= r+1（因为p <= r），j = r+1 >= p-1，成立。
  因此初始化时不变量完全满足。

2. 保持（每次迭代后不变量仍成立） #

假设某次迭代开始时不变量成立，我们执行一次循环体操作，验证下一次迭代开始时不变量依然成立：
循环体的执行步骤如下：

1. 递增i并扫描左半区：
   先执行i = i + 1，然后进入内层循环while i <= r and arr[i] < y，持续递增i直到arr[i] >= y或i > r。
   这一步结束后，所有p < k <= i-1的元素必然都< y——要么是之前满足条件的元素，要么是本次扫描中新增的符合条件的元素，完全符合不变量的第二条。

2. 递减j并扫描右半区：
   执行j = j - 1，然后进入内层循环while j >= p and arr[j] > y，持续递减j直到arr[j] <= y或j < p。
   这一步结束后，所有j+1 <= k <= r的元素必然都> y——要么是之前满足条件的元素，要么是本次扫描中新增的符合条件的元素，完全符合不变量的第三条。

3. 交换指针元素（若i <= j）：
   此时arr[i] >= y，arr[j] <= y。若i <= j，交换arr[i]和arr[j]：

   • 交换后，i位置的元素变为<= y，但不变量的第二条只约束到i-1，因此不影响；
   • j位置的元素变为>= y，不变量的第三条只约束j+1及以后，因此也不影响；
   • 指针边界约束依然满足，因为i和j的位置未超出之前的范围。
     若i > j，则循环直接终止，无需交换。

综上，每次迭代后循环不变量依然成立。

3. 终止（外层循环结束时） #

当i > j时，外层循环终止。此时结合不变量可以推导：

• 所有p < k <= i-1的元素< y，而i > j意味着i-1 >= j，因此所有p < k <= j的元素都< y；
• 所有j+1 <= k <= r的元素都> y；
• arr[j] <= y（因为最后一次j的扫描停在第一个<= y的位置）。

此时执行swap(arr, j, p)，将基准值y从p位置交换到j位置：

• 交换后arr[j] = y；
• 所有p <= k < j的元素< y；
• 所有j+1 <= k <= r的元素> y。

这完全符合快速排序分区的要求：返回的j是基准值的最终位置，左半区元素都小于基准，右半区元素都大于基准。

内容的提问来源于stack exchange，提问作者Dennis