Разрыв между спецификацией и кодом: где живут баги

В теории языков программирования время от времени всплывает одно утверждение: «достаточно подробная спецификация неотличима от кода». Вывод провокационный: граница между описанием того, что программа должна делать, и самим исполнением тоньше, чем кажется. Если спецификация настолько точна, что не оставляет места для двусмысленности, по сути вы уже написали программу.

Это не просто философия. Отсюда следуют практические выводы: как мы строим ПО, какую роль играют спецификации и почему большинство багов — это не ошибки в коде, а пробелы в спецификации. Понимание того, где заканчивается спецификация и начинается реализация, меняет подход к тестированию, типам и корректности.

Откуда на самом деле берутся баги

Спросите разработчика, откуда берутся баги, и он почти наверняка скажет: «из кода». Но исследования дефектов ПО показывают другое: большинство багов возникает в зазоре между намерением и реализацией. Код делает ровно то, что ему велели. Но велели ему не то, потому что спецификация, формальная или неформальная, была двусмысленной, неполной или её неправильно поняли.

Классический пример: в спецификации написано «система должна обрабатывать параллельные запросы». Что значит «обрабатывать»? По порядку? Одновременно? Ставить в очередь, если их слишком много? Что такое «слишком много»? Что происходит с запросами, которые приходят, когда очередь заполнена? Это не детали реализации, а пробелы в спецификации. И каждый оставленный без ответа вопрос — потенциальный баг: разработчик ответит на него неявно, через реализацию, и его ответ может не совпасть с ожиданиями пользователей или других разработчиков.

Степени точности спецификации

Спецификации бывают разными: от неформальных до формальных.

• Естественный язык. «Система входа должна быть безопасной и удобной для пользователя.» Это едва ли спецификация, скорее пожелание. Каждое слово двусмысленно. Что считается «безопасной»? Что считается «удобной»? Это субъективные суждения, замаскированные под требования.
• Структурированный естественный язык. «Если пользователь трижды ввёл неверный пароль в течение 10 минут, заблокировать аккаунт на 30 минут.» Точнее, но всё равно неоднозначно. Считается ли «неверным паролем» пустая отправка? Обязательно ли три попытки подряд? Окно в 10 минут скользящее или фиксированное?
• Сигнатуры типов. authenticate(username: string, password: string) -> Result<User, AuthError>. Это точно описывает интерфейс функции, но ничего не говорит о её поведении. Вы знаете, какие типы поступают на вход и выходят на выход, но не связь между ними.
• Спецификации свойств. «Для всех допустимых пар логин–пароль из базы authenticate возвращает Ok(user), где user.username == username.» Здесь поведение ограничено точнее, с помощью логических кванторов.
• Формальная спецификация. Полная математическая модель поведения системы: каждое состояние, каждый переход, каждый инвариант. На этом уровне спецификация и реализация практически становятся одним и тем же.

Чем ближе вы к формальной спецификации, тем меньше места для двусмысленности и тем меньше места для багов. Но каждый шаг требует больше усилий и специализированных навыков. Практический вопрос: насколько далеко по этому спектру стоит идти в конкретном проекте?

Типы как облегчённые спецификации

Системы типов — самая распространённая форма спецификации в повседневной разработке. Они не описывают поведение, но ограничивают его. Функция, возвращающая Option<User> вместо User, явно говорит: пользователя может не найтись, и компилятор заставит каждого вызывающего обработать эту возможность.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

Языки вроде Rust, Haskell и TypeScript показывают, как выразительные системы типов сокращают разрыв в спецификации без необходимости в обучении формальным методам. Алгебраические типы данных, ограничения на обобщённые типы и исчерпывающий pattern matching вместе задают большую часть поведения программы на уровне типов, и компилятор проверяет это автоматически.

Ключевая мысль: каждая аннотация типа — это спецификация, которая проверяется автоматически. Каждое поведение, которое вы можете закодировать в системе типов, — это класс багов, который у вас никогда не появится.

Property-based тестирование: спецификация поведения

Юнит-тесты — это спецификации на примерах: «для этого конкретного входа ожидаем такой-то выход». Они полезны, но принципиально неполны: тестируются только те случаи, которые пришли в голову. Property-based тестирование переворачивает подход: вы задаёте свойства, которые должны выполняться для всех входов, а фреймворк генерирует случайные данные, чтобы найти нарушения.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

Три свойства в этом тесте не просто проверяют сортировку, они её определяют. Любая функция, удовлетворяющая всем трём свойствам, по определению является корректной сортировкой. Это идея «спецификация как код» в самом практичном виде: вы пишете свойства, которые определяют корректное поведение, а фреймворк проверяет, что ваша реализация им соответствует.

TLA+ и model checking

Для систем, где баги дороги, например распределённых систем, финансовых платформ и критической инфраструктуры, инструменты формальной спецификации вроде TLA+ дают более сильные гарантии. TLA+ (Temporal Logic of Actions) позволяет описать поведение системы как конечный автомат, а затем проверить его model checker-ом: перебрать все возможные исполнения и убедиться, что инварианты выполняются.

Amazon использует TLA+ для верификации алгоритмов в S3, DynamoDB и других критичных сервисах AWS. Компания публично рассказывала о багах, которые практически невозможно было найти тестированием, таких, что проявляются только при определённых чередованиях параллельных операций, случающихся раз на миллионы исполнений.

TLA+-спецификация для протокола консенсуса вроде Raft обычно занимает несколько сотен строк. Она описывает каждый допустимый переход состояний, каждый инвариант (например, «не более одного лидера в терме») и каждое свойство безопасности. Model checker затем перебирает миллиарды путей исполнения и проверяет, что ни один из них не нарушает инвариантов. Это спецификация, которая по-настоящему близка к коду: достаточно точная, чтобы её можно было механически перевести в реализацию.

Проектирование по контракту

Design by Contract (DbC) Бертрана Мейера занимает практичную промежуточную позицию. Каждая функция задаёт предусловия (что должно быть истинно до вызова), постусловия (что функция гарантирует при возврате) и инварианты (что всегда должно быть истинно для объекта). Контракты проверяются во время выполнения в процессе разработки и могут быть отключены в продакшене ради производительности.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

Постусловие о сохранении, то есть что общая сумма денег до и после перевода одинакова, — это как раз тот тип инварианта, который ловит баги, редко покрываемые юнит-тестами. Оно описывает фундаментальное свойство системы (деньги не создаются и не исчезают), которому должна удовлетворять любая корректная реализация.

Практические рекомендации

Полная формальная спецификация для большинства программ не практична. Но сузить разрыв в спецификации можно заметно, используя техники, которые вписываются в обычный процесс разработки.

1. Активно используйте систему типов. Кодируйте ограничения в типах везде, где это возможно. Предпочитайте NonEmptyList вместо List, если список не должен быть пустым. Используйте newtype-обёртки, чтобы отличать UserId от OrderId, даже если оба — строки. Каждое ограничение, закодированное в типах, компилятор проверит бесплатно.
2. Пишите property-based тесты для ключевой логики. Определите инварианты, которые система должна поддерживать, и выразите их как property-тесты. Даже несколько хорошо подобранных свойств ловят баги, которые пропускают тысячи тестов на примерах.
3. Описывайте границы. Самые важные спецификации находятся на границах системы: контракты API, схемы баз данных, форматы сообщений. Используйте OpenAPI, Protocol Buffers или JSON Schema, чтобы сделать их пригодными для машинной проверки.
4. Используйте TLA+ или Alloy для критичных конкурентных систем. Если вы проектируете алгоритм консенсуса, распределённую блокировку или систему финансовых транзакций, стоимость формальной спецификации невелика по сравнению с ценой тонких багов корректности в продакшене.
5. Пишите спецификацию до тестов. Если вы не можете точно сформулировать, как выглядит корректное поведение, вы не сможете его проверить. Потратив 30 минут на ясное описание того, что должна делать функция (все случаи, включая граничные), вы часто выявите проблемы дизайна до того, как напишете хоть строчку кода.

Утверждение, что «достаточно подробная спецификация — это код», не совсем верно. Точнее сказать так: достаточно подробная спецификация убирает место для багов. Разрыв между спецификацией и реализацией — это место, где живёт двусмысленность, а двусмысленность — благодатная почва для багов. Каждый приём, который сужает этот разрыв, будь то типы, свойства, контракты или формальные методы, делает ПО корректнее. Не потому что он предотвращает ошибки кодирования, а потому что предотвращает ошибки в спецификации, из которых обычно и растут ошибки кодирования.