algorithm - 7-1 霍尔分区正确性证明

Question

我正在尝试解决 CLRS（算法简介）中的一些问题，但我遇到了问题 7-1 的问题。b部分（现在）内容如下：

索引 i 和 j 使得我们永远不会访问子数组 A[p ... r] 之外的 A 的元素。

我将如何去证明它？我可以看到指数向中间移动但是......这真的让我的大脑扭曲。解释它不是证据。如果有人能对这个问题有所了解，我将非常感激。

Answer 1

我相信您指的是以下分区算法：

PARTITION(A,p,r)
  x = A[p]
  i = p-1
  j = r+1
  while TRUE
    do repeat j=j-1
         until A[j]<=x
       repeat i=i+1
         until A[i]>=x
       if i<j
         then exchange A[i] and A[j]
         else return j

while 循环的一个合适的不变量是 总是有一个索引 a 使得 A[a] <= x 和 p <= a < j 和一个索引 b 使得 A[b] 使得 A[b]>=x并且 i < b <= r。

你需要证明：

1. 当循环开始时这是真的（提示：选择 a=p 和 b=p）
2. 如果在循环开始时这是真的，那么在循环结束时它仍然是真的。（提示：交换时选择a=j，b=i）

为 while 循环建立不变量后，您可以考虑每个重复循环并显示索引必须保持在允许的范围内。（提示：对于第一个重复循环，尝试证明 j 始终 >= a 其中 a 与原始不变量中的定义相同）