 fox
II/IDEC networks :: habra.14 :: / [Перевод] Доказательство некорректности алгоритма сортировки Android, Java и Python
|
Login |
[#]
[Перевод] Доказательство некорректности алгоритма сортировки Android, Java и Python
habrabot(difrex,1) — All
2015-03-01 18:30:02
Тим Петерс разработал [гибридный алгоритм сортировки Timsort][1] в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем [Джошуа Блох][2] (создатель коллекций Java, именно он, кстати, отметил, что [большинство алгоритмов двоичного поиска содержит ошибку][3]) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды. Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации [сортировки подсчётом][4] и [поразрядной сортировки][5] ([J. Autom. Reasoning 53(2), 129-139][6]) нашим инструментом формальной верификации под названием [KeY][7], мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились. Статья с более полным анализом, а также несколько тестовых программ доступны на [нашем сайте][8]. [Читать дальше →][9]
[1]: http://ru.wikipedia.org/wiki/Timsort
[2]: http://en.wikipedia.org/wiki/Joshua_Bloch
[3]: http://habrahabr.ru/post/203398/
[4]: https://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%80%D1%82%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0_%D0%BF%D0%BE%D0%B4%D1%81%D1%87%D1%91%D1%82%D0%BE%D0%BC
[5]: https://ru.wikipedia.org/wiki/%D0%9F%D0%BE%D1%80%D0%B0%D0%B7%D1%80%D1%8F%D0%B4%D0%BD%D0%B0%D1%8F_%D1%81%D0%BE%D1%80%D1%82%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0
[6]: http://link.springer.com/article/10.1007%2Fs10817-013-9300-y
[7]: http://www.key-project.org/
[8]: http://www.envisage-project.eu/timsort-specification-and-verification/
[9]: http://habrahabr.ru/post/251751/#habracut
habrabot(difrex,1) — All
2015-03-01 18:30:02
Тим Петерс разработал [гибридный алгоритм сортировки Timsort][1] в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем [Джошуа Блох][2] (создатель коллекций Java, именно он, кстати, отметил, что [большинство алгоритмов двоичного поиска содержит ошибку][3]) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды. Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации [сортировки подсчётом][4] и [поразрядной сортировки][5] ([J. Autom. Reasoning 53(2), 129-139][6]) нашим инструментом формальной верификации под названием [KeY][7], мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились. Статья с более полным анализом, а также несколько тестовых программ доступны на [нашем сайте][8]. [Читать дальше →][9]
[1]: http://ru.wikipedia.org/wiki/Timsort
[2]: http://en.wikipedia.org/wiki/Joshua_Bloch
[3]: http://habrahabr.ru/post/203398/
[4]: https://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%80%D1%82%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0_%D0%BF%D0%BE%D0%B4%D1%81%D1%87%D1%91%D1%82%D0%BE%D0%BC
[5]: https://ru.wikipedia.org/wiki/%D0%9F%D0%BE%D1%80%D0%B0%D0%B7%D1%80%D1%8F%D0%B4%D0%BD%D0%B0%D1%8F_%D1%81%D0%BE%D1%80%D1%82%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0
[6]: http://link.springer.com/article/10.1007%2Fs10817-013-9300-y
[7]: http://www.key-project.org/
[8]: http://www.envisage-project.eu/timsort-specification-and-verification/
[9]: http://habrahabr.ru/post/251751/#habracut