# Quicksort Invariant and steps to determine correcteness

I am having trouble with applying to 3 steps needed to proof correctness, most likely because I did not formally study CS or Mathematics and am still learning about loop and class invariants. The three steps:

1. Initialization
2. Maintenance
3. Termination

My understanding of the invariant is that, at the end of the partitioning process, we will have split the array into 3 regions. One where all elements are less than pivot, the pivot itself, and the region where all elements are larger or equal to the pivot.

Assuming the invariant I stated above is correct, I do not see how it is true before, and after the each iteration (which I believe is a requirement for correctness)

private static void sort (Comparable[] a, int lo, int hi){

// a has been shuffled using fisher-yates-knuth

if (hi <= lo)
return;

// pivot is chosen, a[j],  rearranges a[lo:hi], such that all elements  a[lo:j-1] are less than pivot a[j] and all elements a[j+1:hi] are greater than pivot
int partitionIndex = partition(a, lo, hi);

sort(a, lo, partitionIndex - 1);
sort(a, partitionIndex + 1, hi);

}

/**
*
* @param a array to sort
* @param lo start index of segment that needs to be partitioned
* @param hi end index of segment that needs to be partitioned
* @return index of the pivot
*/
private static int partition(Comparable[] a, int lo, int hi){
// arbitrarily choose pivot
Comparable pivot = a[hi];

int partitionIndex = lo;

// scan array from lo to hi - 1, we skip hi because this is the pivot element

// iterate over elements lo to hi - 1, since hi is already pivot there is no need
for (int i = lo; i < hi; i ++){
if (isLessThan(a[i], pivot)){
exchange(a, i, partitionIndex);
partitionIndex++;
}
}
exchange(a, hi, partitionIndex);

// at this point, our array should be partitioned (divided) in three regions

// region 1: pivot should be greater than all elements to its left
// region 2: pivot should be less than or equal to all elements to its right
// region 3: pivot was placed in the middle of the partition (the two regions)
assert leftRegionCorrect(a, lo, partitionIndex) && rightRegionCorrect(a, lo, partitionIndex) && a[partitionIndex] == pivot;

return partitionIndex;

}