Alloy
Формальная верификация · язык и анализатор моделей
создано · обновлено
Способ описать объекты и связи между ними и попросить программу найти небольшой пример, где правило нарушено. Например, правило «у сотрудника ровно один начальник»: программа находит пример, где у одного сотрудника сразу два начальника. Подходит для проверки устройства данных и прав доступа. Запись, как и у TLA+, математическая. Язык создан в группе проектирования ПО при MIT.
Источник: alloytools.org — сайт Alloy
Где встречается · 4
- Vitest или Jest · Спеки и контекст
- Как найти состояние гонки (race condition) в коде · Спеки и контекст
- Чем model checking отличается от тестов · Спеки и контекст
- Какой язык формальной верификации выбрать · Спеки и контекст