Программист
10,7
рейтинг
1 марта 2015 в 16:00

Разработка → Доказательство некорректности алгоритма сортировки Android, Java и Python перевод

Тим Петерс разработал гибридный алгоритм сортировки Timsort в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем Джошуа Блох (создатель коллекций Java, именно он, кстати, отметил, что большинство алгоритмов двоичного поиска содержит ошибку) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды.

Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации сортировки подсчётом и поразрядной сортировки (J. Autom. Reasoning 53(2), 129-139) нашим инструментом формальной верификации под названием KeY, мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились.

Статья с более полным анализом, а также несколько тестовых программ доступны на нашем сайте.

Содержание
  1. Баг в реализации Timsort на Android, Java и Python
    1.1 Воспроизводим баг Timsort на Java
    1.2 Как в принципе работает Timsort?
    1.3 Баг Timsort шаг за шагом
  2. Доказательство (не)корректности Timsort
    2.1 Система верификации KeY
    2.2 Исправление и его формальная спецификация
    2.3 Анализ результатов работы KeY
  3. Предложенные исправления бага к реализациям Timsort на Python и Android/Java
    3.1 Некорректная функция merge_collapse (Python)
    3.2 Исправленная функция merge_collapse (Python)
    3.3 Некорректная функция mergeCollapse (Java/Android)
    3.4 Исправленная функция mergeCollapse (Java/Android)
  4. Заключение: какие из этого следуют выводы?

1. Баг в реализации Timsort на Android, Java и Python


Так в чём же заключается баг? И почему бы вам не попробовать воспроизвести его самим?

1.1 Воспроизводим баг Timsort на Java


git clone https://github.com/abstools/java-timsort-bug.git
cd java-timsort-bug
javac *.java
java TestTimSort 67108864

Если баг присутствует, вы увидите такой результат
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 40
at java.util.TimSort.pushRun(TimSort.java:413)
at java.util.TimSort.sort(TimSort.java:240)
at java.util.Arrays.sort(Arrays.java:1438)
at TestTimSort.main(TestTimSort.java:18)

Видеозапись воспроизведения ошибки


1.2 Как в принципе работает Timsort?


Тimsort — это гибридный алгоритм, который использует сортировку вставкой и сортировку слиянием.

Алгоритм переупорядочивает входной массив слева направо, находя в нём последовательные (неперекрывающиеся) сортированные сегменты («серии», или runs). Если серия короче определённой минимальной длины, она дополняется последующими элементами и сортируется вставкой. Длины созданных серий добавляются в конец массива runLen. Когда новая серия добавляется в runLen, метод mergeCollapse сливает серии, пока три последних элемента в runLen не будут удовлетворять следующей паре условий, которая называется «инвариантом»:

  1. runLen [n-2] > runLen [n-1] + runLen [n]
  2. runLen [n-1] > runLen [n]

Здесь n — это индекс последней серии в runLen. Идея была в том, что проверка этого инварианта для последних трёх серий гарантирует, что все последовательные тройки серий будут ему удовлетворять. В конце сливаются все серии, что даёт в результате полностью отсортированный входной массив.

Из соображений эффективности желательно выделить как можно меньше памяти под runLen, но её должно быть достаточно, чтобы туда заведомо поместились все серии. Если инвариант выполняется для всех серий, длина серий будет расти экспоненциально (даже быстрее, чем числа Фибоначчи: длина каждой серии строго больше суммы длин двух последующих). Так как серии не перекрываются, их потребуется не так много, чтобы полностью отсортировать даже огромный входной массив.

1.3 Баг Timsort шаг за шагом


Из следующего фрагмента кода видно, что реализация mergeCollapse проверяет инвариант для последних трёх серий в runLen:
private void mergeCollapse() {
  while (stackSize > 1) {
    int n = stackSize - 2;
    if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) {
      if (runLen[n - 1] < runLen[n + 1])
         n--;
      mergeAt(n);
    } else if (runLen[n] <= runLen[n + 1]) {
      mergeAt(n);
    } else {
      break; // инвариант установлен
    }
  }
}

К сожалению, этого не достаточно, чтобы все серии удовлетворяли инварианту. Предположим, что runLen содержит такой набор длин перед выполнением mergeCollapse (n=4):
120, 80, 25, 20, 30

На первом проходе цикла while будут объединены серии длиной 25 и 20 (так как 25 < 20 + 30 и 25 < 30):
120, 80, 45, 30

На втором проходе цикла (теперь n=3), мы определяем, что инвариант установлен для последних трёх серий, потому что 80 > 45 + 30 и 45 > 30, поэтому mergeCollapse завершает работу. Но mergeCollapse не восстановил инвариант для всего массива: он нарушается в первой тройке, так как 120 < 80 + 45.

Генератор тестов на нашем сайте позволяет выявить эту проблему. Он создаёт входной массив с множеством коротких серий, при этом их длины не удовлетворяют инварианту, что приводит к падению Timsort. Истинная причина ошибки в том, что из-за нарушения инварианта длины серий растут медленнее, чем ожидалось, в результате чего их количество превышает runLen.length и это приводит к ArrayOutOfBoundsException.

2. Доказательство (не)корректности Timsort


Мы обнаружили, что инвариант mergeCollapse нарушается, когда пытались формально верифицировать Timsort. К счастью, мы также поняли, как его исправить. В итоге нам даже удалось верифицировать исправленную версию, в которой инвариант действительно соблюдается. Но не будем спешить. Для начала разберёмся, что такое формальная верификация и как она выполняется.

2.1 Система верификации KeY


KeY — это платформа дедуктивной верификации однопоточных программ на Java и JavaCard. Она позволяет доказать корректность программ по заданной спецификации. Грубо говоря, спецификация состоит из предусловий (в терминах KeY — requires) и постусловий (в терминах KeY — ensures). Спецификации задаются перед методами, которые их реализуют (например, перед упомянутым выше mergeCollapse()). Спецификация метода также называется его контрактом.

В случае сортировки предусловие просто утверждает, что на вход подаётся непустой массив, а постусловие требует, чтобы результирующий массив был сортирован и являлся перестановкой входного. Система KeY доказывает, что если верифицируемый метод вызвать с входными данными, которые удовлетворяют предусловиям, то метод завершится нормально и результирующее состояние будет удовлетворять постусловию. Это также называется полной корректностью, потому что доказывается и нормальное завершение метода. Как мы увидели, метод java.util.Arrays.sort() из OpenJDK не соблюдает этот контракт, потому что для определённых входных данных он завершается исключением.

Дополнительно используются инварианты классов и объектов, чтобы указать общие ограничения на значения полей. Обычно проверяется согласованность данных или граничные условия:
/*@ private invariant
  @    runBase.length == runLen.length && runBase != runLen;
  @*/

Этот инвариант говорит, что длины массивов runBase и runLen должны совпадать, но в то же время это должны быть два разных массива. Семантика инвариантов подразумевает, что каждый метод на выходе должен не только обеспечивать постусловия своего контракта, но и инварианты его собственного объекта “this”.

В качестве языка спецификаций KeY использует Java Modeling Language (JML). Выражения на нём пишутся как на обычном языке Java, поэтому Java-программисты его легко освоят. Главное расширение JML — это кванторы (\forall T x — для любого T, \exists T x — существует T) и, конечно, специальные ключевые слова для контрактов. Спецификации JML приводятся в комментариях java-файлов перед кодом, к которому они относятся. Ниже приведён простой пример Java-метода с JML-спецификацией:

/*@ private normal_behavior
  @ requires
  @   n >= MIN_MERGE;
  @ ensures
  @   \result >= MIN_MERGE/2;
  @*/

private static int /*@ pure @*/ minRunLength(int n) {
  assert n >= 0;
  int r = 0;      // Становится 1 если хотя бы один единичный бит был удалён сдвигом
  /*@ loop_invariant n >= MIN_MERGE/2 && r >=0 && r<=1;
    @ decreases n;
    @ assignable \nothing;
    @*/
  while (n >= MIN_MERGE) {
    r |= (n & 1);
    n >>= 1;
  }
  return n + r;
}

Контракт minRunLength() содержит одно предусловие: входной параметр должен быть не меньше, чем MIN_MERGE. В этом случае (и только в этом) метод обещает завершиться нормально (не зациклиться и не выбросить исключение) и вернуть значение, которое больше или равно MIN_MERGE/2. Дополнительно метод помечен как pure (чистый). Это означает, что метод не модифицирует кучу.

Ключевой момент в том, что система KeY способна статически доказать контракты подобных методов для любых входных параметров. Как это возможно? KeY производит символьное выполнение верифицируемого метода, то есть, выполняет его, используя символьные значения, так что учитываются все возможные пути выполнения. Но этого недостаточно, потому что символьное выполнение циклов с нефиксированным числом итераций (таких как цикл в mergeCollapse(), где мы не знаем значение stackSize) никогда не завершится. Чтобы символьное выполнение циклов стало конечным, используется логика инвариантов. Например, вышеприведённый метод minRunLength() содержит цикл, спецификация которого выражена инвариантом цикла. Инвариант утверждает, что после каждой итерации выполняется условие n >= MIN_MERGE/2 && r >= 0 && r <= 1, и из этого можно доказать постусловие всего метода. Аннотация decreases (уменьшается) используется, чтобы доказать завершение цикла. В ней указывается выражение, значение которого неотрицательно и строго уменьшается. Конструкция assignable перечисляет объекты кучи, которые могут быть изменены в цикле. Ключевое слово \nothing означает, что куча не модифицируется. И действительно: цикл изменяет только локальную переменную r и аргумент n.

В общем, для формальной верификации недостаточно контрактов методов. Необходимо также приводить инварианты циклов. Иногда очень непросто придумать инвариант, который соблюдается в цикле и при этом достаточно силён, чтобы из него вывести постусловие метода. Без инструментальной поддержки и технологии автоматизированного доказательства теорем вряд ли возможно составить правильные инварианты циклов в нетривиальных программах. На самом деле именно здесь и кроется ошибка создателей Timsort. При определённых условиях цикл в mergeCollapse нарушает следующий инвариант класса Timsort (смотрите раздел 1.3 Баг Timsort шаг за шагом):

/*@ private invariant 
  @   (\forall int i; 0<=i && i<stackSize-4; 
  @                      runLen[i] > runLen[i+1] + runLen[i+2]))
  @*/

Этот инвариант утверждает, что runLen[i] должно быть больше, чем сумма двух последующих элементов, для любых неотрицательных i, меньших stackSize-4. Инвариант не восстанавливается и после цикла, поэтому весь метод mergeCollapse не сохраняет инвариант класса. Следовательно, инвариант цикла не такой строгий, как предполагали разработчики. Это мы и обнаружили в процессе нашей попытки верифицировать Timsort с помощью KeY. Без специального инструмента обнаружить это было бы почти невозможно.

Хотя JML и очень похож на Java, это полноценный язык программирования по контракту, подходящий для полной функциональной верификации Java-программ.

2.2 Исправление и его формальная спецификация


Упрощённая версия контракта, который по задумке авторов должен соблюдаться в mergeCollapse, приведена ниже.
/*@ requires
  @   stackSize > 0 &&
  @   runLen[stackSize-4] > runLen[stackSize-3]+runLen[stackSize-2]
  @   && runLen[stackSize-3] > runLen[stackSize-2];
  @ ensures
  @   (\forall int i; 0<=i && i<stackSize-2; 
  @                     runLen[i] > runLen[i+1] + runLen[i+2])
  @   && runLen[stackSize-2] > runLen[stackSize-1]
  @*/
private void mergeCollapse()

Две формулы в ensures подразумевают, что когда mergeCollapse завершается, все серии удовлетворяют инварианту, приведённому в разделе 1.2. Мы уже видели, что этот контракт не выполняется в текущей реализации mergeCollapse (раздел 1.3). Теперь мы приводим исправленную версию, которая соблюдает контракт:

private void newMergeCollapse() {
  while (stackSize > 1) {
    int n = stackSize - 2;
    if (n > 0   && runLen[n-1] <= runLen[n] + runLen[n+1] || 
        n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1]) {
      if (runLen[n - 1] < runLen[n + 1])
        n--;
    } else if (n<0 || runLen[n] > runLen[n + 1]) {
      break; // инвариант установлен
    }
    mergeAt(n);
  }
}

Основная идея этой версии — проверять, что инвариант соблюдается для четырёх последних серий в runLen вместо трёх. Как мы увидим ниже, этого достаточно, чтобы длины всех серий удовлетворяли инварианту после завершения mergeCollapse.

Первый шаг в доказательстве контракта для исправленной версии mergeCollapse — это найти подходящий инвариант цикла. Вот его упрощённая версия:

/*@ loop_invariant
  @  (\forall int i; 0<=i && i<stackSize-4; 
  @             runLen[i] > runLen[i+1] + runLen[i+2])
  @  && runLen[stackSize-4] > runLen[stackSize-3])
  @*/

Интуитивно инвариант цикла утверждает, что все серии кроме, возможно, последних четырёх, удовлетворяют условию. При этом заметим, что цикл завершается (по оператору break), только если последние четыре серии тоже ему удовлетворяют. Таким образом, можно гарантировать, что все серии удовлетворяют инварианту.

2.3 Анализ результатов работы KeY


Когда мы подаём на вход KeY исправленную версию mergeCollapse вместе с контрактом и инвариантом цикла, система производит символьное выполнение цикла и генерирует условия верификации: формулы, из истинности которых следует, что контракт mergeCollapse выполняется. Следующая (упрощённая) формула показывает главное условие доказательства корректности mergeCollapse, сгенерированное KeY:



Формула утверждает, что из условий в скобках, которые истинны после завершения цикла, должно следовать постусловие mergeCollapse. Понятно, откуда взялись выражения в скобках: оператор break, который завершает цикл, выполняется только когда они все истинны. Мы формально доказали эту формулу (и все прочие условия верификации) с помощью KeY в полуавтоматическом режиме. Ниже приведён набросок доказательства:

Доказательство. Формула runLen[stackSize-2] > runLen[stackSize-1] из постусловия mergeCollapse прямо следует из n >= 0 ==> runLen[n] > runLen[n+1].

Докажем следующую формулу:

\forall int i; 0<=i && i<stackSize-2; runLen[i] > runLen[i+1] + runLen[i+2].

Возможны следующие варианты значения i:

  • i < stackSize-4: соответствует инварианту цикла
  • i = stackSize-4: следует из n>1 ==> runLen[n-2] > runLen[n-1] + runLen[n]
  • i = stackSize-3: следует из n>0 ==> runLen[n-1] > runLen[n] + runLen[n+1]

Это доказательство показывает, что новая версия mergeCollapse завершается только когда все серии удовлетворяют инварианту.

3. Предложенные исправления бага к реализациям Timsort на Python и Android/Java


Наш анализ ошибки (включая исправление mergeCollapse) был отправлен, рассмотрен и принят в багтрекер Java.

Баг присутствует как минимум в версии Java для Android, OpenJDK и OracleJDK: во всех используется одинаковый код Timsort. Также баг присутствует в Python. В следующих разделах приводятся оригинальная и исправленная версии.

Как было сказано выше, идея исправления очень проста: проверять, что инвариант выполняется для последних четырёх серий в runLen, а не только для трёх.

3.1 Некорректная функция merge_collapse (Python)


Timsort для Python (написан на C с использованием Python API) доступен в репозитории subversion – Алгоритм также описан здесь.

Версия Timsort для Java была портирована с CPython. Версия на CPython содержит ошибку, разработанная для поддержки массивов вплоть до 264 элементов, также содержит ошибку. Однако на современных машинах вызвать ошибку переполнения массива невозможно: алгоритм выделяет 85 элементов для runLen, и этого хватает (как показывает наш анализ в полной статье) для массивов, содержащих не более 249 элементов. Для сравнения, мощнейший на сегодняшний день суперкомпьютер Tianhe-2 обладает 250 байтами памяти.

/* The maximum number of entries in a MergeState's 
 * pending-runs stack.
 * This is enough to sort arrays of size up to about
 *     32 * phi ** MAX_MERGE_PENDING
 * where phi ~= 1.618.  85 is ridiculously large enough, 
 * good for an array with 2**64 elements.
 */
#define MAX_MERGE_PENDING 85

merge_collapse(MergeState *ms)
{
    struct s_slice *p = ms->pending;

    assert(ms);
    while (ms->n > 1) {
        Py_ssize_t n = ms->n - 2;
        if (n > 0 && p[n-1].len <= p[n].len + p[n+1].len) {
            if (p[n-1].len < p[n+1].len)
                --n;
            if (merge_at(ms, n) < 0)
                return -1;
        }
        else if (p[n].len <= p[n+1].len) {
                 if (merge_at(ms, n) < 0)
                        return -1;
        }
        else
            break;
    }
    return 0;
}

3.2 Исправленная функция merge_collapse (Python)


merge_collapse(MergeState *ms)
{
    struct s_slice *p = ms->pending;

    assert(ms);
    while (ms->n > 1) {
        Py_ssize_t n = ms->n - 2;
        if (     n > 0   && p[n-1].len <= p[n].len + p[n+1].len
            || (n-1 > 0 &&  p[n-2].len <= p[n].len + p[n-1].len)) {
            if (p[n-1].len < p[n+1].len)
                --n;
            if (merge_at(ms, n) < 0)
                return -1;
        }
        else if (p[n].len <= p[n+1].len) {
                 if (merge_at(ms, n) < 0)
                        return -1;
        }
        else
            break;
    }
    return 0;
}

3.3 Некорректная функция mergeCollapse (Java/Android)


Ошибка полностью аналогична ошибке в Python:
   private void mergeCollapse() {
        while (stackSize > 1) {
            int n = stackSize - 2;
            if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) {
                if (runLen[n - 1] < runLen[n + 1])
                    n--;
                mergeAt(n);
            } else if (runLen[n] <= runLen[n + 1]) {
                mergeAt(n);
            } else {
                break; // Инвариант установлен
            }
        }
    }

3.4 Исправленная функция mergeCollapse (Java/Android)


Исправление аналогично приведённому выше для Python.
[UPDATE 26/2: мы изменили код по сравнению с исходной версией статьи. Старый код был эквивалентен, но содержал избыточную проверку и отличался по стилю. Спасибо всем, кто обратил внимание!]
   private void newMergeCollapse() {
     while (stackSize > 1) {
       int n = stackSize - 2;
       if (   (n >= 1 && runLen[n-1] <= runLen[n] + runLen[n+1])
           || (n >= 2 && runLen[n-2] <= runLen[n] + runLen[n-1])) {
                if (runLen[n - 1] < runLen[n + 1])
                    n--;
            } else if (runLen[n] > runLen[n + 1]) {
                break; // Инвариант установлен
            }
            mergeAt(n);
        }
    }

4. Заключение: какие из этого следуют выводы?


При попытке верифицировать Timsort нам не удалось установить инвариант объекта сортировки. Анализируя причины неудачи, мы обнаружили в реализации Timsort ошибку, которая приводит к ArrayOutOfBoundsException для определённых входных данных. Мы предложили исправление ошибочного метода (без ощутимого снижения производительности) и формально доказали, что исправление корректно и ошибки больше нет.

Из этой истории, помимо собственно найденной ошибки, можно сделать несколько наблюдений.
  1. Зачастую программисты считают формальные методы непрактичными и/или далёкими от реальных задач. Это не так: мы нашли и исправили ошибку в программном обеспечении, которым пользуются миллиарды пользователей каждый день. Как показал наш анализ, найти и исправить такой баг без формального анализа и инструмента для верификации было бы практически невозможно. Ошибка долгие годы жила в стандартной библиотеке языков Java и Python. Её проявления замечали ранее и даже думали, что исправили, но в действительности добились только того, что ошибка стала возникать реже.
  2. Хотя маловероятно, что такая ошибка возникнет случайно, легко представить, как можно её использовать для атаки. Вероятно, в стандартных библиотеках популярных языков программирования кроются и другие незамеченные ошибки. Может быть, стоит заняться их поиском до того как они причинят вред или будут использованы злоумышленниками?
  3. Реакция разработчиков Java на наш отчёт в некотором смысле разочаровывает. Вместо того, чтобы использовать нашу исправленную (и верифицированную!) версию mergeCollapse(), они предпочли увеличить выделенный размер runLen до «достаточного» размера. Как мы показали, вовсе не обязательно было так делать. Но теперь каждый, кто использует java.utils.Collection.sort() будет вынужден тратить больше памяти. Учитывая астрономическое число программ, использующих настолько базовую функцию, это приведёт к заметным дополнительным затратам энергии. Мы можем только догадываться, почему не было принято наше решение: возможно разработчики JDK не удосужились прочитать наш отчёт полностью и поэтому не поняли суть исправления и решили не полагаться на него. В конце концов, OpenJDK разрабатывает сообщество, в значительной степени состоящее из добровольцев, у которых не так много времени.


Какие из этого следуют выводы? Мы были бы счастливы, если бы наша работа послужила начальной точкой для более тесного взаимодействия между исследователями формальных методов и разработчиками открытых программных платформ. Формальные методы уже успешно применяются в Amazon и Facebook. Современные языки формальной спецификации и инструменты формальной верификации не являются такими уж запутанными и суперсложными в изучении. Постоянно улучшается их юзабилити и автоматизация. Но нам нужно больше людей, которые бы пробовали, тестировали и использовали наши инструменты. Да, потребуются некоторые усилия, чтобы начать писать формальные спецификации и верифицировать код, но это не сложнее, чем, например, разобраться, как использовать компилятор или средство сборки проектов. Но речь идёт о днях или неделях, а не месяцах или годах. Ну как, вы принимаете вызов?

С наилучшими пожеланиями,
Стайн де Гув, Юриан Рот, Франк де Бур, Ричард Бубель и Райнер Хенле.

Благодарности


Работа частично поддержана проектом седьмой рамочной программы Евросоюза FP7-610582 ENVISAGE: Engineering Virtualized Services.
Эта статья не была бы написана без поддержки и вежливых напоминаний Амунда Твейта! Также мы хотим поблагодарить Беруза Нобакта за то, что предоставил нам видео, демонстрирующее ошибку.

Envisage logo
Перевод: Stijn de Gouw
Тагир Валеев @lany
карма
475,2
рейтинг 10,7
Программист
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Реклама

Самое читаемое Разработка

Комментарии (26)

  • –9
    А это перевод статьи?
    • +13
      Да. Сверху так и написано — перевод.
  • +6
    Кстати, аналогичный баг нашли и пофиксали на Хаскеле.
  • +1
    Возможна ли эксплуатация этого бага in the wild для атаки отказа в обслуживании, как считаете?
    • +7
      Вряд ли, должно быть очень нетривиальное стечение обстоятельств. Во-первых, ошибка проявляется для довольно больших массивов из миллионов элементов, причём они должны быть специально сконструированы. Нечасто злоумышленник контролирует такой объём данных. Во-вторых, прямое последствие ошибки — это падение сортировки с исключением. При этом массив остаётся недосортированным, но данные все в нём лежат. Тут должна быть дополнительная проблема на атакуемой системе. К примеру, некорректная обработка исключения, в результате чего возникнет потеря данных. Или игнорирование исключения и выполнение на массиве дополнительного алгоритма, который предполагает, что массив отсортирован, и ведёт себя неадекватно, если это не так.
      • 0
        Это в Яве падение сортировки с исключением. А в Питоне?
        • +12
          А в питоне нужны слишком большие массивы ("Версия на CPython содержит ошибку,… алгоритм выделяет 85 элементов для runLen, и этого хватает (как показывает наш анализ в полной статье) для массивов, содержащих не более 2^49 элементов. Для сравнения, мощнейший на сегодняшний день суперкомпьютер Tianhe-2 обладает 2^50 байтами памяти.").
          Для массива байтов 2^49 = 512 терабайт.
  • +13
    А в Python поправили всё честно: bugs.python.org/issue23515 автор алгоритма там даже отписался.
  • 0
    А разве нельзя делать функцию бинарного поиска на этапе сортировки массива?
    Зачем массив нужно сначала отсортировать(упорядочить), а затем делать в нём поиск?
    • +5
      Часто бывает, что необходимо в одном и том же массиве искать много раз. Поэтому проще сперва один раз отсортировать, а затем быстро искать бинарным поиском. Если вам надо один раз поискать, проще вообще не сортировать, а перебрать все элементы линейно.
      • 0
        Спасибо!
  • 0
    java.utils.Array.sort() -> java.utils.Arrays.sort()
    • 0
      Исправил, спасибо.
      • 0
        Давайте еще раз, я ошибся в package name java.util.Arrays.sort()

        docs.oracle.com/javase/7/docs/api/java/util/Arrays.html
        • +2
          Кто-нибудь объясните человеку, далекому от Java, есть ли какой-то принцип, по которому выбирают, будет ли имя модуля в единственном числе или во множественном? Почему util в единственном, а Arrays во множественном?
          • +1
            Потому что util сокращение от utility, utils не имеет смысла.
            А так обычно Lists заведует листами, List это как раз объект листа.
            Аналогично есть Collections, Objects, Sets. Часть из них правда в Гуаве, но принцип понятен.
            Аналогично Arrays заведует массивами, просто тут аналогичного объекта Array просто нет, но конвенция понятна.
            • +1
              Понятно, спасибо. Я больше по части C++ и для меня все наоборот: в util дофига утилит, поэтому его надо назвать utils, от utilities, что является довольно распространенным сокращением. Функции, заведующие списком я бы сделал статическими методами класса List, а для Array сделал бы класс только со статическими методами для единообразия.
              • +2
                java.util — это package
                Collections, Objects и т.д. — это мода в Java по неимингу утильных классов(для Collection и Objects соответственно)

                Почему это не сделали статическими методами? Скорее всего, потому что это не относится к сущностям, а именно утилиты. Ну и для разделения кода.
            • +1
              Оффтоп: В Java переносят хорошие практики из Guava — в Java 7 Objects появился, в Java 8, по моему, дополнили классы по работе с коллекциями. В общем, не может не радовать :)
              • +1
                Это не совсем так, то есть они действительно сделали Objects, но явно теоретики ибо допускают глупые косяки, что идею убивает. Например, как раз в тему, статический метод сравнения называется в Гуаве equal, а в Яве equals. И если гуавовскую версию можно сократить статик импортом и писать equal(a, b). То с явой не пройдет изза коллизии с обычным equals, не статическим. А полная форма слижком тяжеловесна. Правда, и в последней Гуаве почемуто этот метод переехал в MoreObjects. Но это так, к слову, ибо не мешает.
  • +4
    Много плюсов за статью, но ни одного комментария о самом инструменте формального анализа! Ведь это отличная вещь с великолепными потенциалом — один раз описываем контракт для метода и не беспокоимся о его содержимом — всё и так будет проверяться :)
    А вообще кто-нибудь пользовался подобными вещами? Я так понял, это подобие контрактного программирования. Только более мощное. В IDEA есть аннотация Contract, которая позволяет выполнить простые проверки входных и выходных данных — описываем с помощью этой аннотации контракт для метода (что будет при подаче тех или иных значений), а дальше IDE сама проверят, что метод соответствует этому контракту.
    • +3
      Ну да, что-то похожее. В принципе объявление метода — уже мало-мальский контракт: вы говорите, какие аргументы каких типов метод принимает и какого типа результат вернёт, и сам компилятор следит за соблюдением контракта. Дальнейшее улучшение — аннотации типа jsr305 (Nonnull, Nonnegative), jcip (Immutable), контракты в IDEA и т. д. JML по сути существенное развитие этого подхода. Я сам не использовал, но могу предположить, что полная верификация в KeY может выполняться довольно долго и не всегда ответ будет типа «да/нет», чаще вы увидите набор дополнительных условий, которые KeY вывел, но сам доказать не смог. Кроме того, в описании контракта можно допустить ошибку так же, как в реализации. Поэтому в повседневной практике вряд ли разумно использовать такой инструмент. А вот для проверки алгоритмически сложного кода, который редко меняется — вполне сгодится.

      JML, кстати, и по-другому можно использовать — например, генерировать по контракту случайные тесты и убеждаться, что контракт выполняется.

      Собственно, авторы писали статью (и я переводил) не только с целью показать клёвый баг, но и чтобы прорекламировать это научное направление. Глядишь, кто-нибудь заинтересуется и что-нибудь новенькое откроет :-)
  • +1
    Помнится, писал в университете такие формальные спецификации для всяких алгоритмов на PVS (никакого отношения к часто всплывающей здесь PVS Studio, насколько я понимаю), KeY выглядит на порядок удобнее, хотя и на тех же принципах, похоже, работает.

    Вообще формальные спецификации это очень мило и полезно, но в случае с PVS мозг мне изрядно взрывали, когда приходилось специфицировать операторы и функции, чтобы заработало всё остальное, бинарные операции например не были встроены, а когда доказываешь валидность shift-or… ахаха… хаха… ха…
  • 0
    Не понял героизма авторов (в оригинале куча заумных формул).
    Чтобы написать правильный вариант, достаточно элементарной аккуратности.
    Обозначим последовательность элементов в стеке цифрами 1,2,3,4.
    Тройки 1,2,3 и 2,3,4 удовлетворяют некоторому соотношению — инварианту. (Двойки тоже, но их опускаем).
    Добавляем к стеку элемент 5. Пусть тройка на конце (3,4,5) не удовлетворяет инварианту, выясняем, что сливать надо 3 и 4, обозначим результат как А. Теперь содержимое стека 1,2, А,5. Тройка на конце (2, А,5) удовлетворяет инварианту. Но какого хрена считать, что 1,2, А теперь тоже удовлетворяет инварианту?? Ясно, что нужно ее теперь проверять.

    • +6
      Во-первых, из ваших рассуждений лишь следует, что проверки трёх последних элементов недостаточно, но не следует, что проверки четырёх элементов достаточно (хотя это тоже можно доказать на пальцах). Во-вторых, тут получается вроде Колумбова яйца: когда решение известно, оно выглядит тривиальным. В классе TimSort почти 1000 строк и 15 методов. Найдёте ли вы с помощью элементарной аккуратности ошибку в таком объёме кода? А ведь авторы исследования даже не знали, есть ли ошибка.

      Куча заумных формул — это да, математики же, они так разговаривают :-)
      • 0
        Ну да, я счел очевидным, что новое значение (А) не может испортить других инвариантов.

        В целом я ориентировался на синтез правильного алгоритма, а не анализ готового чужого. Последнее, конечно, гораздо геморойнее.
        А автоматически — так вообще супер.

Только зарегистрированные пользователи могут оставлять комментарии. Войдите, пожалуйста.