TLA+
Формальная верификация · автор Лесли Лэмпорт
создано · обновлено
Способ описать, как система ведёт себя шаг за шагом, настолько точно, что описание можно проверить программой, как чертёж проверяют до стройки. Например, по чертежу денежного перевода находят, что при сбое между списанием и зачислением деньги пропадают, и делают это до написания кода. Запись похожа на математические формулы, поэтому порог входа выше, чем у Quint. Автор языка Лесли Лэмпорт.
Источник: Страница TLA+ Лесли Лэмпорта
Где встречается · 4
- Vitest или Jest · Спеки и контекст
- Как найти состояние гонки (race condition) в коде · Спеки и контекст
- Чем model checking отличается от тестов · Спеки и контекст
- Какой язык формальной верификации выбрать · Спеки и контекст