7-1 Hoare分区正确性证明

Question

我正在尝试解决CLRS(算法介绍)中的一些问题，我在问题7-1中遇到了麻烦。b部分(目前)内容如下:

下标i和j永远不能访问A中的元素在子数组A[p…]r] .

我该如何证明呢?我可以看到指数向中间移动，但是。这真把我弄糊涂了。解释它并不是证明。

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]>=x and i <= r.

你需要显示:

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

一旦为while循环建立了不变量，就可以考虑每个repeat循环，并显示索引必须保持在允许的范围内。(提示:对于第一个重复循环，尝试证明j总是>= a，其中a在原始不变式中定义)