Какой язык формальной верификации выбрать, зависит от того, что ломается: TLA+ и Quint описывают поведение системы шаг за шагом, Alloy описывает объекты и связи между ними. Quint записывается как обычный код, TLA+ и Alloy как формулы. Для правил продукта во времени берут Quint, для строгих доказательств TLA+, для данных и прав Alloy.
Чем отличаются TLA+, Alloy и Quint: одна задача, три языка
У всех трёх языков общая идея: правила системы записывают отдельно от кода, а программа сама ищет в них нарушение. Если нарушение есть, она показывает, как до него дойти. Это проверка моделей, и у неё в каждом случае свой язык и своя проверяющая программа. TLA+ придумал Лесли Лэмпорт для описания параллельных и распределённых систем. Alloy создан в группе проектирования ПО при MIT. Quint придуман как современная альтернатива TLA+ для инженеров.
Сводка: TLA+, Alloy и Quint рядом
Главное отличие: что именно описывают. TLA+ и Quint описывают поведение системы шаг за шагом: корзина, оплата, заказ, и что может пойти не так между шагами. Так находят гонки и потерянные данные. Alloy описывает структуры и связи: кто кому подчиняется, у кого какие права. Он ищет небольшой пример, где правило нарушено, например сотрудника с двумя начальниками. Остальные различия вытекают из этого.
| TLA+ | Alloy | Quint | |
|---|---|---|---|
| Что описывают | поведение системы шаг за шагом, особенно параллельное и распределённое | объекты и связи между ними и то, как они меняются | поведение шаг за шагом, как у TLA+ |
| Запись | математическая | логика отношений | похожа на обычный код |
| Чем проверяют | TLC или Apalache | Alloy Analyzer, он подбирает структуры под ограничения | TLC или Apalache, есть быстрый случайный прогон |
| Что показывает | цепочку шагов до нарушения | пример структуры, где правило нарушено | цепочку шагов до нарушения |
| Зрелость | с 1999 года, больше книг и примеров | с 1997 года, своё сообщество | с 2021 года, моложе |
| Кому подходит | тем, кому нужны строгие гарантии | тем, кто проектирует данные и права доступа | командам продукта без математической подготовки |
Как читать таблицу по строкам. «Что описывают» самая важная: от неё зависит выбор. «Запись» определяет порог входа: у Quint он ниже всех, у TLA+ и Alloy нужно привыкнуть к формулам. «Чем проверяют» напоминает, что языки опираются на разные программы-проверяльщики: Apalache и TLC подходят и TLA+, и Quint, а у Alloy свой анализатор. «Что показывает» объясняет, что вы получите на выходе: цепочку шагов или пример структуры. «Зрелость» подсказывает, где больше примеров и людей, у которых можно спросить.
Граница между языками не абсолютная. В шестой версии Alloy добавил изменяемое состояние и временную логику, то есть научился описывать и шаги во времени. А Quint и TLA+ можно использовать для структур данных. Поэтому выбор определяется тем, что в вашей системе ломается чаще: порядок событий или устройство связей.
Чем TLA+ отличается от Alloy
TLA+ создал Лесли Лэмпорт, и в его основе лежит мысль, что точнее всего описывать вещи простой математикой. Он ищет цепочку шагов, на которой правило ломается, например двойную оплату и два заказа. Alloy ищет пример структуры, в которой правило нарушено, и проверяет свойства модели, строя контрпримеры. Для порядка событий берут TLA+, для связей и прав доступа Alloy.
Чем TLA+ отличается от Quint
Описывают они одно и то же, различается запись. Quint задуман как синтаксис, удобный инженерам, а проверяют обе записи одни и те же программы. TLC перебирает состояния по одному, а Apalache символьный и рассматривает все цепочки до заданной длины.
Чем Alloy отличается от Quint
У Alloy своя программа проверки: Alloy Analyzer берёт ограничения модели и находит структуры, которые им удовлетворяют. Quint такой программы не имеет, его проверяют две другие, TLC и Apalache. Поэтому выбор часто сводится к вопросу, что ломается: связи между объектами или порядок шагов.
Что выбрать: TLA+, Alloy или Quint
Правила продукта во времени и команда без математики: берите Quint. Нужны строгие доказательства для сложной распределённой системы: берите TLA+ и закладывайте время на обучение. Нужно проверить устройство данных или права доступа: берите Alloy. Идеи из одной записи можно перенести в другую, потому что правила остаются теми же. Как Quint соотносится с тестовыми движками вроде Jest и QUnit, разобрано в статье Quint против QUnit и TLA+, а примеры найденных им ошибок есть в статье про гонки и потерянные данные.
Частые вопросы
TLA+ описывает поведение системы шаг за шагом и ищет цепочку шагов, где правило ломается. Alloy описывает объекты и связи между ними и ищет пример структуры, где правило нарушено.
Описывают они одно и то же, различается запись: Quint похож на обычный код, а TLA+ записывают математической нотацией. Проверяют обе записи одни и те же программы, TLC и Apalache.
Для правил продукта во времени и команды без математики берите Quint, для строгих доказательств по сложной распределённой системе TLA+, для устройства данных и прав доступа Alloy.
TLA+ и Quint проверяют программы TLC и Apalache. У Alloy свой анализатор, Alloy Analyzer: он берёт ограничения модели и находит структуры, которые им удовлетворяют.