Formele methoden leggen fout in Java’s sorteeralgoritme bloot

In 2002 ontwikkelde Tim Peters een nieuw hybride sorteeralgoritme voor de Python-programmeertaal. Hij combineerde ideeën uit traditionele merge sort– en insertion sort-algoritmes en maakte handig gebruik van het idee dat datasets in de dagelijkse praktijk vaak al gedeeltelijk gesorteerd zijn. Bovendien buit het algoritme op slimme wijze de cache- en geheugenarchitectuur van computers uit, waardoor het zeer efficiënt werkt. Vanwege deze aantrekkelijke eigenschappen werd Timsort al snel vertaald naar Java (als java.util.Collections.sort en java.util.Arrays.sort).

Vandaag de dag is Timsort wijdverspreid als het standaard sorteeralgoritme in Java. Het is dus van groot belang dat het correct is en niet crasht of andere problemen veroorzaakt. Omdat het daarnaast vrij complex is, vonden we dit een mooie uitdaging om onze tanden in te zetten. Begin dit jaar hadden we succesvol een project afgerond om counting- en radix sort-implementaties in Java formeel te analyseren, met ondersteunende software hiervoor, en nu wilden we een volgende stap zetten.