Subject Infrastructure Repository
I. Language Agnostic Overview
This code is part of the Quicksort algorithm, one of the fastest and most efficient sorting algorithms in use today. Quicksort is extremely common, used explicitly in many programs and implicitly in others, since it is part of the Java libraries. Since it so frequently used, correctness is required, and proving this correctness for all situations is worthwhile.
This specific implementation is from Saswat Anand, Corina S. Pasareanu, and Willem Visser. Symbolic execution with abstract subsumption checking. SPIN Workshop on Model Checking of Software, 2006. This was in turn implemented from: Tomas Ball. A theory of predicate-complete test coverage and generation. Technical report, Microsoft Research, 2004.
II. Java Specific Overview
This class divides an array into upper and lower halves, using the first element (a) as a pivot. It does this by moving all elements whose value is larger than the pivot to after all the elements whose value is smaller than the pivot. Ideally, this pivot will be the median value, and after partitioning the array would be evenly divided between low and high values. It should also be noted that the algorithm uses an in-place partitioning scheme to save memory.
As the name indicates, this class is implemented with an array rather than a linked list or tree of any kind. This implementation has several advantages and disadvantages, and a future study may wish to consider the same algorithm with different underlying data structures.
The invariant is realized through a basic assert and function.