先上伪代码
HOARE-PARTITION(A, p, r)
x = A[any number in p..r]
i = p - 1
j = r + 1
while true
repeat
j = j - 1
until A[j] ≤ x
repeat
i = i + 1
until A[i] ≥ x
if i < j
exchange A[i] with A[j]
else return j 提醒
与Lomuto Partition不同，在Hoare Partition中，pivot元素是包含在分出的两个区中的。
Hoare Partition的作用效果是：给定一个pivot元素，将数组分为两个区域，其中一个区域的值总是不大于另一区域的值。这个算法不能保证pivot元素位于何处。
正确性证明
约定
- p小于等于r
- 分出的两个区中可能有一个是空的
- a..b表示从a到b，inclusive；a>b则代表空集，其中一切性质成立
首先是几个循环不变式
1）在整个循环中我们不会进行A[i]操作，其中i<p；也不会进行A[j]操作，其中j>r
初始化：进入while循环前i=p-1，j=p+1，在第一次A[i]和A[j]前i=p，j=r，所以A[i]操作访问A[p]，A[j]操作访问A[r]。
保持：i随循环递增，j随循环递减，所以A[i]操作不可能访问p之前的元素，A[j]操作不可能访问r之后的元素。
2）在整个循环中我们不会进行A[i]操作，其中i>r；也不会进行A[j]操作，其中j<p
初始化同1。
保持：只需证“在整个循环中A[i..r]总包含不小于x的元素，在整个循环中A[p..j]总包含不大于x的元素”。以下证明前者，后者请读者自证。
2.1）在整个循环中A[i..r]总包含不小于x的元素
初始化显然（x是A中的一个元素）。
保持：当i和j停下（由初始化可知必至少停一次）且i<j时，此时A[i]与A[j]交换，不小于x的A[i]被交换到后方，从而维持了循环不变式。
终止：当i和j停下且i不小于j时，循环结束。
3）在整个循环中A[p..i]不大于x，A[j..r]不小于x
读者自证不难。
证明正文
由（1）和（2）知i,j总在p..r内。
由（3）知每次i<j的迭代中A[p..i]中的任意元素小于或等于A[j..r]中的任意元素。
在最后一次迭代中，A[p..i]中除A[i]外的任意元素小于或等于A[j..r]中除A[j]外的任意元素。
而此时i不小于j，则：
当i=j时，易得A[i]=A[j]=x（由i和j移动的终止条件直接可得），则A[p..i]中的任意元素小于或等于A[j..r]中的任意元素，则A[p..j]中的任意元素小于或等于A[j+1..r]中的任意元素。
当i>j时，A[p..j]中的任意元素（显然，不包含A[i]）小于或等于A[j+1..r]中的任意元素（显然，也不包含A[j]）。
没有评论:
发表评论