Композиция корректности. Как собрать рабочую систему из сервисов с подтверждённой спецификацией
«Программы должны быть написаны так, чтобы их корректность можно было доказать, а не угадать тестированием.»
— Niklaus Wirth, Systematic Programming
Это финальная статья серии про корректность программ. В предыдущих мы по кирпичу собирали модуль, сервис и спецификацию:
- «Модульность программы» — модуль как чёрный ящик с одним входом и одним выходом.
- «Правильность программы» — корректность по построению, не по тестированию.
- «README — это продукт» — документация как контракт для четырёх потребителей.
- «Сколько компонентных тестов нужно сервису» — формула и логический вывод.
- «Компонентные тесты на практике» — семь тестов на passkey-demo-api.
- «Два скилла дисциплины» — vertical slice, конструкторы вместо фабрик, головной модуль как пайп.
Сервис в результате этой дисциплины имеет спецификацию, подтверждённую тестами в изоляции. Юнит-тесты по формуле «1 + ветки антецедента» подтверждают, что каждый модуль ведёт себя по своему контракту. Компонентные сценарии в Gherkin через Docker Compose подтверждают, что сервис как чёрный ящик ведёт себя по OpenAPI/AsyncAPI и по карте режимов отказа в README.
Корректность при этом достигается проектированием, не тестированием. Тестирование, как помним из Дейкстры, может только показать наличие ошибок, но не их отсутствие. Тесты в нашей дисциплине — это исполняемая документация контракта, которую машина периодически сверяет с реальным кодом. Подтверждение, а не доказательство.
Но в индустрии один такой сервис никому не нужен. Нужна система — десять, двадцать, сто сервисов, которые ходят друг к другу через сеть, и эта система должна работать.
И вот здесь индустрия ставит поверх всей пирамиды ещё один этаж: интеграционные тесты, e2e на Playwright, системные стенды, регрессионные прогоны на стейджинге. Тысячи сценариев. Часы прогонов. Десятки человеко-месяцев на поддержку.
В этой статье покажу, что весь этот этаж — компенсация отсутствия двух простых вещей: машиночитаемого контракта и канареечного деплоя. При наличии обоих корректность системы выводится из корректности сервисов и совместимости их контрактов. Без e2e, без стейджинга, без бесконечной регрессии.
