Где светится инструмент проверки ключа?

Question

Какие примеры кода демонстрируют силу KeY?

подробности

С таким количеством доступных инструментов Формального метода мне было интересно, где KeY лучше, чем его конкурент, и как? Некоторые читаемые примеры кода были бы весьма полезны для сравнения и понимания.

Обновления

Просматривая веб-сайт KeY, я нашел примеры кода из книги - есть ли где-нибудь подходящий пример кода?

Кроме того, я нашел статью об ошибке, которую KeY обнаружил в mergeCollapse Java 8 в TimSort. Что такое минимальный код от TimSort, который демонстрирует силу KeY? Однако я не понимаю, почему при проверке модели не удается найти ошибку - битовый массив с 64 элементами не должен быть слишком большим для обработки. Могут ли другие инструменты дедуктивной проверки обнаружить ошибку?

Существует ли установленный конкурс проверки с подходящими примерами кода?

Answer 1

Это очень сложный вопрос, поэтому на него еще не ответили после того, как его уже задавали более года назад (и хотя мы из сообщества KeY хорошо знаем об этом...).

Сила взаимодействия

Во-первых, я хотел бы отметить, что KeY, по сути, является единственным инструментом, позволяющим интерактивно проверять Java-программы. Хотя многие доказательства работают автоматически, и у нас есть достаточно мощные автоматические стратегии, иногда требуется взаимодействие, чтобы понять, почему доказательство не удается (слишком слабые или даже неправильные спецификации, неправильный код или "просто" неспособность проверки) и добавить подходящие исправления или усиления,

Отзыв от проверочной инспекции

Особенно в случае неспособности проверяющего (спецификация и программа в порядке, но проблема слишком сложна для того, чтобы проверяющий автоматически преуспел), взаимодействие является мощной функцией. Многие программы проверки (например, OpenJML, Dafny, Frama-C и т. Д.) Полагаются на решатели SMT в бэкэнде, которые они подают со многими более или менее небольшими условиями проверки. Статус проверки для этих условий затем сообщается пользователю, в основном, как пройденный или неудачный - или тайм-аут. Когда утверждение не удалось, пользователь может изменить программу или уточнить спецификации, но не может проверить состояние доказательства, чтобы вывести информацию о том, почему что-то пошло не так; этот стиль иногда называют "автоактивным", а не интерактивным. Хотя это может быть довольно удобно во многих случаях (особенно когда доказательства проходят, поскольку решатели SMT могут действительно быстро что-то доказывать), может быть сложно добыть вывод средства решения SMT для получения информации. Даже сами решатели SMT не знают, почему что-то пошло не так (хотя они могут привести к контрпримеру), поскольку им просто дают набор формул, для которых они пытаются найти противоречие.

TimSort: сложная алгоритмическая проблема

Для доказательства TimSort, которое вы упомянули, нам пришлось использовать много взаимодействий, чтобы заставить их пройти. Возьмем, к примеру, метод сортировки алгоритма mergeHi, который был проверен одним из самых опытных известных мне опытных пользователей KeY. В этом доказательстве 460К узлов проверки потребовалось 3К взаимодействия с пользователем, состоящее из множества простых, таких как сокрытие отвлекающих формул, а также из 478 определений квантификатора и около 300 сокращений (введение в лемму онлайн). Код этого метода содержит множество сложных Java-функций, таких как вложенные циклы с помеченными разрывами, целочисленные переполнения, битовая арифметика и т. Д.; в частности, существует множество потенциальных исключений и других причин ветвления в дереве доказательств (именно поэтому, кроме того, в доказательстве также использовались пять приложений правил слияния состояний вручную). Рабочий процесс для доказательства этого метода в основном заключался в том, чтобы на некоторое время попробовать стратегии, проверить состояние доказательства после этого, сократить время доказательства и ввести полезную лемму, чтобы уменьшить общую работу по проверке и начать заново; иногда квантификаторы создавались вручную, если стратегии не могли найти правильный экземпляр непосредственно сами по себе, и ветви дерева доказательств были объединены для решения проблемы взрыва состояния. Я хотел бы просто заявить, что проверка этого кода (по крайней мере, в настоящее время) невозможна с помощью автоактивных инструментов, где вы не можете направлять средство проверки таким образом, а также не можете получить правильную обратную связь для того, чтобы знать, как ее вести.

Сила ключа

В заключение я бы сказал, что KeY сильна в доказательстве сложных алгоритмических задач (таких как сортировка и т. Д.), Где у вас есть сложные количественные инварианты и целочисленная арифметика с переполнениями, и где вам нужно найти экземпляры количественных выражений и небольшие леммы на лету, проверяя и взаимодействуя с доказательством состояния. Подход KeY к полуинтерактивной проверке также в целом превосходит случаи, когда SMT решает тайм-аут, так что пользователь не может определить, что-то не так или требуется дополнительная лемма.

KeY может, конечно, также доказать "простые" проблемы, однако там вам нужно позаботиться о том, чтобы ваша программа не содержала неподдерживаемую функцию Java, такую ​​как числа с плавающей запятой или многопоточность; Кроме того, библиотечные методы могут быть серьезной проблемой, если они еще не определены в JML (но эта проблема также применима и к другим подходам).

Текущие разработки

В качестве дополнительного замечания я также хотел бы отметить, что в настоящее время KeY все больше и больше трансформируется в платформу для статического анализа различных типов свойств программы (не только функциональной корректности программ Java). С одной стороны, мы разработали такие инструменты, как символьный отладчик выполнения, который могут также использовать неспециалисты для изучения поведения последовательной Java-программы. С другой стороны, в настоящее время мы заняты рефакторингом архитектуры системы, позволяющей добавлять внешние интерфейсы для языков, отличных от Java (в нашем внутреннем проекте "KeY-RED"); кроме того, предпринимаются постоянные усилия по модернизации внешнего интерфейса Java, чтобы также поддерживались более новые языковые функции, такие как Lambdas и т. д. Мы также изучаем реляционные свойства, такие как корректность компилятора. И хотя мы уже поддерживаем интеграцию сторонних решателей SMT, наше интегрированное логическое ядро ​​все еще будет там, чтобы поддерживать понимание проверочных ситуаций и ручных взаимодействий для случаев, когда SMT и автоматизация терпят неудачу.

Пример кода TimSort

Так как вы попросили пример кода... Я не могу точно вспомнить пример кода, показывающий силу KeY, но, возможно, для того, чтобы дать вам представление о сложности mergeHi в алгоритме TimSort, здесь укороченная выдержка с некоторыми комментариями (полный метод имеет около 100 строк кода):

private void mergeHi(int base1, int len1, int base2, int len2) {
  // ...
  T[] tmp = ensureCapacity(len2); // Method call by contract
  System.arraycopy(a, base2, tmp, 0, len2); // Manually specified library method

  // ...

  a[dest--] = a[cursor1--]; // potential overflow, NullPointerException, ArrayIndexOutOfBoundsException
  if (--len1 == 0) {
    System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
    return; // Proof branching
  }
  if (len2 == 1) {
    // ...
    return; // Proof branching
  }

  // ...
outer: // Loop labels...
  while (true) {
    // ...
    do { // Nested loop
      if (c.compare(tmp[cursor2], a[cursor1]) < 0) {
        // ...
        if (--len1 == 0)
          break outer; // Labeled break
      } else {
        // ...
        if (--len2 == 1)
          break outer; // Labeled break
      }
    } while ((count1 | count2) < minGallop); // Bit arithmetic

    do { // 2nd nested loop
      // That's one complex statement below...
      count1 = len1 - gallopRight(tmp[cursor2], a, base1, len1, len1 - 1, c);
      if (count1 != 0) {
        // ...
        if (len1 == 0)
          break outer;
      }
      // ...
      if (--len2 == 1)
        break outer;

      count2 = len2 - gallopLeft(a[cursor1], tmp, 0, len2, len2 - 1, c);
      if (count2 != 0) {
        // ...
        if (len2 <= 1)
          break outer;
      }
      a[dest--] = a[cursor1--];
      if (--len1 == 0)
        break outer;
      // ...
    } while (count1 >= MIN_GALLOP | count2 >= MIN_GALLOP);
    // ...
  }  // End of "outer" loop
  this.minGallop = minGallop < 1 ? 1 : minGallop;  // Write back to field

  if (len2 == 1) {
    // ...
  } else if (len2 == 0) {
    throw new IllegalArgumentException(
        "Comparison method violates its general contract!");
  } else {
    System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
  }
}

Конкурс верификации

VerifyThis - это признанный конкурс для инструментов верификации на основе логики, который будет проходить в седьмой раз в 2019 году. Конкретные задачи для прошлых событий можно загрузить из раздела "Архив" на веб-сайте, на который я ссылаюсь. В 2017 году в нем приняли участие две команды KeY. В этом году победителем стал Why3. Интересное наблюдение состоит в том, что была одна проблема, Pair Insertion Sort, которая была упрощенной и оптимизированной версией Java, для которой ни одной команде не удалось проверить реальную оптимизированную версию на сайте. Тем не менее, команда KeY завершила это доказательство в течение нескольких недель после события. Я думаю, что это подчеркивает мою точку зрения: ключевые доказательства сложных алгоритмических задач требуют своего времени и опыта, но они, вероятно, будут успешными благодаря объединенной силе стратегий и взаимодействия.