Большинство багов прячутся в разрыве между «что должно делать» и «что реально делает»
Сначала пишете код, потом тесты, потом обнаруживаете, что код был неправ. Это стандартный цикл. Поэтому отладка поглощает половину сроков большинства проектов.
Box Structure переворачивает это. Вы определяете поведение до написания, проверяете это определение математически, а затем переводите в код слой за слоем. Результат — модуль, корректный по построению, а не потому что тесты случайно прошли.
Это звучит невозможно, пока не увидишь, насколько мал каждый слой.
Что такое Box Structure?
Box Structure описывает программный модуль на трёх уровнях абстракции, каждый из которых является строгим уточнением предыдущего:
- Black box: Какой stimulus даёт какой response? Нет состояния. Нет реализации. Только чистая функция от истории к выходу.
- State box: Какое состояние запоминает модуль и как каждый stimulus трансформирует это состояние и порождает response?
- Clear box: Собственно код.
Вы проектируете извне внутрь. Black box — это контракт. State box — это модель данных. Clear box — это код. На каждом шаге вы доказываете, что нижний слой удовлетворяет верхнему, прежде чем двигаться дальше.
Это не документация post factum. Black box и state box — формальные спецификации. Они и есть проектирование. Код пишется в последнюю очередь.
Black Box: история определяет всё
Black box определяет модуль через историю stimulus и его response. Response на любой stimulus зависит от каждого предшествующего stimulus.
Рассмотрим простой rate limiter на основе token bucket. Спецификация black box гласит:
| Stimulus | Condition on History | Response |
|---|---|---|
request(n) | tokens available >= n | grant(n) |
request(n) | tokens available < n | deny |
add_tokens(k) | any history | no response, update history |
Black box не говорит, как отслеживаются tokens. Она говорит: при данной истории stimuli это требуемый response.
Это можно проверить до написания кода. Запишите последовательности stimuli, вычислите ожидаемые responses вручную и проверьте, что спецификация ведёт себя правильно. Никакого компилятора. Никакого test runner. Только логика.
State Box: добавление памяти без добавления предположений
State box уточняет black box, вводя переменную состояния, которая делает историю неявной. Вместо того чтобы таскать с собой полную историю stimuli, модуль запоминает сжатое представление.
Для rate limiter state box вводит tokens — текущее количество доступных tokens. Спецификация становится:
| Stimulus | Precondition on State | Response | New State |
|---|---|---|---|
request(n) | tokens >= n | grant(n) | tokens - n |
request(n) | tokens < n | deny | tokens (unchanged) |
add_tokens(k) | any | no response | tokens + k |
Ключевой шаг — доказать, что эта state box эквивалентна black box. Переменная состояния tokens должна точно представлять соответствующую историю. Если применение правил black box даёт те же responses, что и счётчик state box, уточнение верно.
Это доказательство обычно короткое. Вы проверяете спецификацию на страницу, а не кодовую базу в тысячу строк.
Clear Box: код, который не может удивить
Clear box — это реализация. Она пишется на структурированном языке без goto и скрытого control flow. Каждая clear box строится из последовательности, альтернативы (if-then-else) и итерации (while, for).
Вот реализация clear box на Python:
class TokenBucket:
def __init__(self, capacity: int, refill_rate: float):
self.capacity = capacity
self.tokens = capacity
self.refill_rate = refill_rate
self.last_refill = time.monotonic()
def _refill(self) -> None:
now = time.monotonic()
elapsed = now - self.last_refill
added = int(elapsed * self.refill_rate)
if added > 0:
self.tokens = min(self.capacity, self.tokens + added)
self.last_refill = now
def request(self, n: int) -> str:
self._refill()
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
self.tokens = min(self.capacity, self.tokens + k)Обратите внимание: _refill не было в state box. Время не существует в black box и state box. Эти модели предполагают, что tokens появляются волшебным образом при вызове add_tokens. Clear box должна заполнить этот пробел.
Именно здесь живёт большинство багов. State box говорит, что tokens увеличивается на k. Clear box также должна обрабатывать непрерывное пополнение и ограничение ёмкости, оставаясь при этом согласованной со state box.
Как Cleanroom доказывает корректность без запуска тестов
В Cleanroom вы не пишете unit tests для clear box. Вы выполняете verification.
Для каждой control structure вы записываете предикат, который должен выполняться до и после её исполнения. Для последовательности S1; S2 вы доказываете, что postcondition S1 влечёт precondition S2. Для if-then-else вы доказываете, что обе ветви удовлетворяют общей postcondition. Для цикла while вы находите invariant и доказываете, что он выполняется при входе, сохраняется на каждой итерации и влечёт желаемую postcondition при завершении цикла.
Это не proof assistant. Это карандаш и бумага. Если вы когда-либо неформально доказывали, что рекурсивная function завершается, вы уже сделали 90 процентов доказательства Cleanroom.
Почему большинство команд этим не пользуются
Очевидное возражение — время. Написание black box, state box и ручного доказательства звучит медленнее, чем просто написать код и исправить баги.
Харлан Миллс, разработавший Cleanroom в IBM, измерил обратное. Команды Cleanroom поставляли код с дефектами на порядок меньше, чем контрольные группы, а общее время разработки было короче, потому что они почти не проводили времени в дебаггере.
Менее очевидное возражение — культурное. Box Structure заставляют думать до набора текста. Большинство разработчиков находят это некомфортным. Спецификация кажется бюрократией. Это не так. Это проектирование. В Cleanroom проект записан в нотации, достаточно точной для проверки, а не в диаграмме, которую первый черновик реализации игнорирует.
Когда Box Structure стоят накладных расходов
Не нужно так специфицировать каждую утилитарную function. Box Structure раскрываются там, где баг стоит дороже времени написания спецификации: payment processing, authorization, distributed consensus, протоколы и workflow engines. Они также помогают командам, которые повторно выпускают в production баги одной категории и никогда не ловят их в тестах.
Лёгкий способ начать
Не нужно внедрять весь процесс Cleanroom. Заимствуйте идею Box Structure для одного модуля.
Выберите function, которая вызывала проблемы в production. Напишите её black box: таблицу inputs, conditions и expected outputs. Не смотрите на существующий код. Пишите, что она должна делать, а не что делает.
Затем напишите state box. Какое состояние ей нужно? Как каждый input трансформирует это состояние? Сравните с реализацией. Где они расходятся, там вы нашли баг или недокументированное предположение.
Вот минимальный шаблон на Python, который можно адаптировать:
"""
Black Box Specification: Rate Limiter
Stimuli: request(n), add_tokens(k)
History: sequence of all stimuli received
Rules:
1. After any sequence of stimuli, tokens available =
sum(add_tokens.k) - sum(grant.n)
2. request(n) grants iff tokens available >= n
3. tokens available never exceeds capacity
State Box Refinement:
State: tokens (integer, 0 <= tokens <= capacity)
Invariant: tokens accurately represents available tokens
"""
class TokenBucket:
"""Clear box implementation of the rate limiter state box."""
def __init__(self, capacity: int):
self.capacity = capacity
self.tokens = capacity
def request(self, n: int) -> str:
if n <= 0:
raise ValueError("request must be positive")
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
if k < 0:
raise ValueError("cannot add negative tokens")
self.tokens = min(self.capacity, self.tokens + k)Комментарии — это спецификация. Код — это реализация. Хранение их в одном файле делает уточнение наглядным и доступным для review.
Настоящая ценность — разделение ответственности
Box Structure — не магия. Они не поймают все баги. То, что они делают, — навязывают дисциплину, которую большинство процессов разработки пропускает: определять, что значит «корректно», до построения.
Black box отделяет контракт модуля от его внутренностей. State box отделяет модель данных от кода. Clear box отделяет реализацию от доказательства. У каждого слоя одна задача, и вы проверяете её, прежде чем перейти к следующему.
Вот почему это должно вас волновать. Разрыв между «что должно делать» и «что делает» — там, где живут ваши баги, а Box Structure — систематический способ закрыть этот разрыв до написания единого теста.
Если хотите углубиться, книга Миллса «Cleanroom Software Engineering» и оригинальные технические отчёты IBM до сих пор остаются самыми ясными источниками. Идеи стары. Баги, которые они предотвращают, — нет.