Автор: Денис Буздалов · Heisenbug
Денис Буздалов работает в ИСП РАН с 2010 года: верификация авиационной электроники самолётов, тестирование криптопротоколов по формальным моделям, зависимые типы. Человек, который думает о корректности систем профессионально.
8 апреля 2022 года самолёт TAP Air Portugal в Копенгагене ушёл на второй круг в нестандартной ситуации — и левый двигатель не свернул реверс тяги. ПО было корректно сертифицировано. Баг проявился после 95 миллионов посадок и не воспроизводился ни в одной другой конфигурации. Самолёты так и продолжили летать с этим ПО спустя годы — исправление планировалось к 2025 году. Буздалов задаёт с этого вопрос: что вообще значит «хорошо протестировано», если такое возможно?
Его ответ: хорошее тестирование должно ставить систему в ситуации, о которых автор тестов даже не подумал. Property-based testing это умеет — описываешь свойства, а не примеры, фреймворк ищет опровержение на случайном входе. Но есть класс задач, где случайный вход почти всегда бессмысленен: сгенерировать программу, которая корректно тайпчекается, или граф с нетривиальными инвариантами наугад — значит получить 99% мусора. Буздалов показывает, как зависимые типы закрывают эту дыру: инвариант входных данных кодируется в типе, и генератор выводится автоматически через DepTyCheck.
Кому смотреть: всем, кто строит системы, где ошибки дорого стоят и плохо воспроизводятся вручную — не только авторам компиляторов, но и разработчикам протоколов, финансовых движков, встроенного ПО, любых систем с нетривиальными инвариантами на входе.
Из этого можно взять в работу: сформулировать для своей системы одно свойство вместо набора примеров и запустить на нём property-based тест. Не для сложных структур — просто как первый шаг к тому способу думать о тестировании, который Буздалов описывает.
Инцидент с TAP Air Portugal разбирается подробно: уход на второй круг — это команда, а не состояние; cross-wind bounce; за 0,18 секунды, пока шла команда, правое шасси было на земле, левое в воздухе — и именно в этот момент левый двигатель не свернул реверс тяги. Была резервная подсистема, которая сделала auto idle, поэтому обошлось. Буздалов уточняет: ПО прошло сертификацию, комбинация условий не проверялась, потому что никто о ней не думал. Именно это и есть провал тестирования — не потому что тестов мало, а потому что тесты придумывают люди.
Property-based testing устроен иначе: описываешь свойства — roundtrip, идемпотентность, инварианты — и фреймворк генерирует вход сам. Одна спецификация находит ошибки в разных местах, высокоуровневое свойство вскрывает низкоуровневый баг. Shrinking сжимает найденный контрпример до минимального воспроизводящего случая. Ключевое — ты не придумываешь ситуации, ты придумываешь критерий правильности.
Трудность возникает, когда входные данные сами по себе несут инварианты. Генерировать программы на TypeScript-диалекте наугад бессмысленно: почти все не пройдут типизацию ещё до теста. Нужны именно корректно тайпчекающиеся программы — а писать для них генератор руками долго и хрупко.
Зависимые типы (dependent types) решают это на уровне системы типов: если тип SortedNatList гарантирует отсортированность, любое значение этого типа уже является отсортированным списком. DepTyCheck на Idris 2 выводит генератор из такого типа автоматически — без ручного кода. Та же логика для типизированных программ: описываешь в типе «программа, которая проходит typecheck», получаешь генератор семантически корректных программ.
На реальном TypeScript-диалекте с JIT и компилятором этот подход нашёл assertion failed в оптимизаторе (lse.cpp:851) — через свойство «семантически корректная программа должна компилироваться без падений». Буздалов честен в финальной оценке: инструментальная поддержка зачаточная, методы спецификации не отработаны, есть проблемы со скоростью. Но связка работает. И это, пожалуй, главное — мы только в начале пути к тестированию, которое само находит то, о чём мы не думали.