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