Воркшоп: TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов
Разрабатывать конкурентные системы сложно. Самые плохие ошибки закладываются в алгоритм, не находятся никакими тестами, и ждут своей уникальной последовательности событий, чтобы взорваться и всё испортить. Но находить такие ошибки можно, даже не написав ни строчки кода на Go -- если воспользоваться методами формальной верификации. Один из таких методов — разработанный Лесли Лампортом формализм TLA+ и инструмент верификации TLC -- идеально подходит верификации конкурентных систем на Go. Мы поговорим про TLA+/TLC, про PlusCal — транслируемый в TLA+ язык спецификации алгоритмов специально для инженеров, а также про практики применения TLA+/TLC в проектах на Go. В ходе воркшопа мы напишем и разберем несколько простых низкоуровневых моделей алгоритмов работы с каналами в Go, а также попробуем разобрать относительно высокоуровневую модель сервиса. Вводная часть: • TLA+/TLC: практичный инструмент форма... Воркшоп будет проходить в среде MS Visual Studio Code ( /). Вам понадобится плагин TLA+ ( , и, возможно, плагин для Golang ( Исходники слайдов, а также исходные тексты этого воркшопа: Трансляция кода: