算法导论 QuickSort

#include <iostream>
#include <algorithm>

using namespace std;

int Partition(int iArr[], int iFront, int iRear)
{
int iTemp=iArr[iRear], i=iFront;

for (int j=iFront; j<iRear; j++)
if (iArr[j]<=iTemp)
{
swap(iArr[i], iArr[j]);
i++;
}
swap(iArr[i], iArr[iRear]);
return i;
}

void QuickSort(int iArr[], int iFront, int iRear)
{
if (iFront<iRear)
{
int iTemp=Partition(iArr, iFront, iRear);

QuickSort(iArr, iFront, iTemp-1);
QuickSort(iArr, iTemp+1, iRear);
}
}

int main()
{
int iArr[8];

for (int i=0; i<8; i++) cin>>iArr[i];
QuickSort(iArr, 0, 7);
for (int i=0; i<8; i++) cout<<iArr[i]<<' ';
cout<<endl;
return 0;
}

用循环不变式证明函数Partition的性质：

循环不变式：
1）如果iFront<=k<i，则iArr[k]<=iTemp；
2）如果i<=k<j，则iArr[k]>iTemp；
3）如果k=iRear，则iArr[k]=iTemp。

初始化：在for循环的第一轮迭代开始之前，有i=iFront和j=iFront。于是不存在k使得iFront<=k<i，同样不存在k使得i<=k<j，因此，循环不变式的头两个条件显然满足。而iTemp被初始化为iArr[iRear]，使得循环不变式的第三个条件也满足。
保持：假设循环不变式成立，则在每轮迭代开始时，有k∈[iFront, i)使得iArr[k]<=iTemp，k∈[i, j)使得iArr[k]>iTemp，k=iRear使得iArr[k]=iTemp。当iArr[j]<=iTemp时，首先交换iArr[i]和iArr[j]，于是有k∈[iFront, i]使得iArr[k]<=iTemp，k∈[i, j]使得iArr[k]>iTemp，所以当i、j均自增1，即下一轮迭代开始时，循环不变式成立；当iArr[j]>iTemp时，唯一的操作即让j自增1，显然循环不变式将在下一轮迭代时成立。
终止：循环终止时，j=iRear。根据循环不变式，有k∈[iFront, i)使得iArr[k]<=iArr[iRear]，k∈[i, iRear)使得iArr[k]>iArr[iRear]。

函数Partition最后一步交换了iArr[i]和iArr[iRear]，于是使得数组iArr中位于iArr[i]左边的元素小于iArr[i]，位于iArr[i]右边的元素大于iArr[i]。