Чем model checking отличается от тестовQuint, QUnit и TLA+

Чем Quint отличается от QUnit: два похожих названия

QUnit — движок для тестов на JavaScript, из той же семьи, что Jest и Vitest. Вы пишете функцию, затем тест с входом и ожидаемым ответом, и движок говорит, совпало или нет. Quint — язык, на котором описывают, как система должна себя вести. Программа сама перебирает все возможные ходы и ищет среди них те, где правило ломается. Путаница возникает из-за названия, а по сути это программы разных классов. Сравнение самих тестовых движков есть в статье Jest, Vitest или QUnit.

Как выглядит тест QUnit. Он берёт готовую функцию, например сложение, подаёт в неё один и два и сверяет ответ с тройкой: assert.equal(add(1, 2), 3), этот пример есть на сайте QUnit. Если ответ верный, тест проходит. Всё, что тест знает о мире, — вход и ожидаемый ответ, которые вы выбрали заранее.

Модель на Quint устроена иначе: в ней нет функции и ответа. Вы описываете, в каких состояниях бывает система, какие действия переводят её из одного состояния в другое и какие правила должны выполняться всегда. Quint сам запускает такую модель, симулирует её и проверяет до выпуска кода. Поэтому для него неважно, написан код или нет: он проверяет замысел, а не реализацию.

Таблицу удобно читать по строкам. В строке «Что проверяет» видна главная разница: тест отвечает на вопрос «правильно ли работает эта функция на этих данных», модель отвечает на вопрос «возможна ли вообще ситуация, которую правила запрещают». Тест ограничен тем, что вы придумали. Модель ограничена тем, что вы в неё положили.

Quint или Jest и Vitest: что проверяет тест, а что модель

Тестовый движок находит ошибку на тех входах, которые вы придумали. Если вы не подумали о двух администраторах одновременно, тест про них не напишется, и ошибка останется. Модель устроена иначе: она сама строит сочетания шагов, включая такие, которые никому не пришли в голову, и показывает первое, где правило нарушилось.

Что тест ловит хорошо: ошибку в самой функции, например неверный расчёт скидки или неправильный разбор даты. Здесь вход известен заранее, и тест быстро показывает, что сломалось. Что тест пропускает: гонки и другие ошибки, которые возникают только в определённом порядке событий. В примерах из практики так нашлись вход и выход администратора, пересекшиеся во времени, и падение посреди записи встречи. Ни одно из этих действий по отдельности не ошибочно, поэтому тест на каждое из них проходит.

Слабое место Quint в том, что он проверяет модель, а не код. Если модель описана неточно, она докажет что-то о выдуманной системе. Поэтому модель сверяют с реальными случаями, которые уже подтвердили, и хранят в ней пару «как есть и как надо». Подробно об этом в статье про модели.

Чем Quint отличается от TLA+ и Alloy

TLA+ и Alloy — формальные языки того же рода: в них тоже описывают правила и ищут их нарушения. Они старше Quint и лучше описаны в книгах. Но в TLA+ запись математическая, и новичку нужно время, чтобы её читать. Quint придуман как более доступная запись для той же задачи: она похожа на обычный код, и её читают инженеры без математической подготовки. Подробное сравнение всех трёх языков есть в статье TLA+, Alloy или Quint.

Что значит «одни и те же программы». Quint можно проверять двумя программами: TLC и Apalache. TLC — самая первая проверяющая программа для TLA+: она перебирает состояния по одному, поэтому для Quint ей нужен перевод модели в TLA+. Перебор предсказуем, но мир должен быть небольшим.

Apalache встроен в Quint: он переводит модель в условия и спрашивает решатель Z3. Проверять он умеет цепочки только до заданной длины, поэтому его «ок» значит «нарушений нет в пределах этой длины». TLA+ проверяют теми же двумя программами, а у Alloy свой анализатор. Кроме проверки, у Quint есть быстрый случайный прогон: он ищет нарушения выборочно и не доказывает, что их нет.

Каждый из трёх языков опирается на свою идею. TLA+ построен на мысли Лесли Лэмпорта, что точнее всего описывать систему простой математикой. Alloy описывает развивающиеся структуры и программу для их исследования. Quint даёт ту же задачу в записи, понятной инженерам: описание можно запускать, симулировать и проверять до выпуска кода.

Зрелость играет роль, когда нужны тяжёлые доказательства: большие системы, строгие гарантии для распределённых протоколов. Первая версия языка Alloy появилась в 1997 году. TLA+ создал Лесли Лэмпорт, по данным Википедии, язык описан в 1999 году. Проверяющая программа Apalache начата в 2015 году, а репозиторий Quint создан в 2021, по данным GitHub. Поэтому у TLA+ около 27 лет истории, а у Quint около пяти.

За эти годы для TLA+ накопились книги, курсы и разборы реальных систем, а у Quint их меньше. Зато язык развивается быстро: правки в репозиторий проекта вносили накануне даты этой статьи. Для правил продукта вроде «приватная запись не уходит в общее хранилище» глубина доказательств нужна реже, а читаемость важнее.

Что выбрать: Quint, тесты или TLA+

Выбор определяется вопросом, а не любимой программой. Если вопрос «верно ли работает эта функция», берите тест. Если вопрос «может ли в какой-то последовательности событий нарушиться правило», берите модель. Если вам нужны гарантии на уровне распределённого протокола, берите TLA+ и закладывайте время на обучение.

Как они работают вместе

На практике тесты и модели стоят рядом. Тест защищает конкретную функцию от поломки при правках. Модель защищает правило, которое пересекает несколько функций и зависит от порядка событий. Когда модель находит цепочку шагов, из неё получается короткий тест-регрессия: он падает на старом коде и проходит на исправленном.

Так модель отдаёт тестам то, что нашла, а тесты держат это в коде. Подробный разбор находок, пары «как есть и как надо» и проверки самих проверок есть в основной статье про Quint, а про границы контекстов, для которых пишутся модели, в статье про агентов на контекст.

Частые вопросы