Proving JDK's Dual Pivot Quicksort Correct
Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt, Mattias Ulbrich
Sorting is a fundamental functionality in libraries, for which efficiency is
crucial. Correctness of the highly optimized implementations is often taken
for granted. De Gouw et al. have shown that this certainty is deceptive by
revealing a bug in the Java Development Kit (JDK) implementation of TimSort.
We have formally analysed the other implementation of sorting in the JDK
standard library: A highly efficient implementation of a dual pivot quicksort
algorithm. We were able to deductively prove that the algorithm implementation
is correct. However, a loop invariant which is annotated to the source code
does not hold. This paper reports on how an existing piece of non-trivial
Java software can be made accessible to deductive verification and
successfully proved correct, for which we use the Java verification engine
KeY.