0
\$\begingroup\$

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;

}
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.