Cleanroom software engineering даёт 0,1 дефекта на тысячу строк кода. Средний показатель по отрасли — от 10 до 50. Подвох в том, что полный Cleanroom требует разделить команду на авторов и верификаторов, писать формальные спецификации перед каждым модулем и запрещать разработчикам запускать собственный код, пока отдельная команда тестирования не проведёт его статистическую валидацию.

Большинство инженерных менеджеров смотрят на этот процесс, быстро прикидывают численность и решают, что качество не стоит overhead. Они отчасти правы. Полный процесс Cleanroom тяжеловесен. Но лежащие в его основе принципы легковесны, и вы можете внедрить их, не нанимая армию верификаторов и не запрещая cargo test.

Что на самом деле такое Cleanroom

Cleanroom — это процесс разработки ПО, созданный в IBM в 1970-х годах Харланом Миллсом. Название пришло из производства полупроводников: вы предотвращаете условия, при которых возникают дефекты, вместо того чтобы выявлять их постфактум. Основное утверждение — программное обеспечение может быть корректным по построению, если проектировать его достаточно тщательно, чтобы ошибки были невозможны ещё до написания кода.

Метод опирается на три практики: инкрементальная разработка под статистическим управлением процессами, функционально-теоретическое проектирование со структурами box, и статистическое usage testing, выполняемое отдельной командой. Эти три практики взаимозависимы. Нарушьте одну — остальные потеряют силу.

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

Где на самом деле живёт overhead

80% overhead, которого люди боятся, исходят из двух конкретных требований.

Первое — правило no-execution. В полном Cleanroom разработчик, написавший код, не компилирует его, не запускает и не пишет unit tests. Отдельная команда верификации занимается всем выполнением. Это заставляет разработчиков продумывать каждый случай до написания, и именно поэтому код работает с первого раза. Но при этом вам придётся удвоить инженерную численность или разделить существующую команду на две группы, которые будут друг на друга обижаться.

Второе — шаг формальной верификации. Перед написанием clear box implementation команда составляет black box specification и state box refinement, а затем вручную доказывает, что state box эквивалентен black box. Это доказательство карандашом и бумагой, а не proof assistant. Оно работает, но требует времени и обучения, которых у большинства команд нет.

Третья практика — инкрементальная разработка со статистическим управлением процессами — на самом деле бесплатна, если вы уже делаете спринты. Вы поставляете небольшие инкременты, измеряете плотность дефектов на инкремент и останавливаете процесс, когда инкремент превышает целевой показатель дефектов, чтобы выяснить, что пошло не так с методом. Это просто data-driven ретроспективы со строгим определением “done.”

Прагматичное подмножество: сохранить структуру, избавиться от бюрократии

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

Вот что оставить.

Пишите контракт до кода. Не формальную спецификацию в нотации Z. Просто чёткое описание inputs, outputs, preconditions и postconditions. Если вы не можете записать, что означает корректность, вы не можете написать корректный код.

Явно кодируйте state machines. Большинство багов живут в state transitions, которые разработчик считал невозможными. Определите свои состояния и переходы в таблице или структуре данных до написания логики.

Пусть кто-то другой тестирует вашу логику. Разделение авторства и верификации — самая мощная идея Cleanroom. Вам не нужна отдельная команда. Вам нужен один человек, который не писал код, чтобы спроектировать тестовые случаи. Когда вы тестируете свой собственный код, вы тестируете свои собственные предположения.

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

Вот что отбросить.

Отбросьте правило no-execution. Позвольте разработчикам запускать собственный код. Дисциплина сначала рассуждать ценна, даже если вы позволяете себе быструю sanity check после. Смысл в том, чтобы думать перед запуском компилятора, а не притворяться, что компилятора не существует.

Отбросьте формальное ручное доказательство. Если вы не пишете авионическое ПО, доказательство карандашом и бумагой — это overkill. Замените его на property-based tests и type-driven design. Это механизированные версии того же рассуждения, и они работают в CI.

Отбросьте требование статистического usage testing. Полный Cleanroom тестирует по usage profiles, а не по code coverage. Это отлично, если у вас есть данные. Если нет — property-based testing и mutation testing дают почти ту же уверенность с помощью инструментов, которые вы уже используете.

Легковесный workflow Cleanroom на Python

Вот как это выглядит на практике для одного модуля. Начните с контракта.

"""
Black Box: Token Bucket Rate Limiter

Stimuli: request(n), add_tokens(k)
Precondition: n > 0, k >= 0, capacity > 0
Postcondition:
  - request(n) grants iff available tokens >= n
  - request(n) reduces available tokens by n if granted
  - add_tokens(k) increases available tokens by k, capped at capacity
  - available tokens never negative, never exceeds capacity
"""

Затем закодируйте state machine.

from enum import Enum, auto

class RateLimitState(Enum):
    READY = auto()      # tokens >= 1, requests may grant
    DEPLETED = auto()   # tokens == 0, requests deny

# Transitions depend on token count, not external events
# READY -> DEPLETED when tokens reach 0
# DEPLETED -> READY when tokens added above 0

Затем напишите реализацию.

import time
from dataclasses import dataclass

@dataclass
class TokenBucket:
    capacity: int
    tokens: int
    refill_rate: float
    last_refill: float

    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) -> bool:
        if n <= 0:
            raise ValueError("request must be positive")
        self._refill()
        if self.tokens >= n:
            self.tokens -= n
            return True
        return False

    def add_tokens(self, k: int) -> None:
        if k < 0:
            raise ValueError("cannot add negative tokens")
        self.tokens = min(self.capacity, self.tokens + k)

Контракт живёт в docstring. State machine явная. Реализация короткая и верифицируема инспекцией. Это не полный Cleanroom. Это и не cowboy coding.

Шаг верификации, который вы действительно можете сделать

В полном Cleanroom отдельная команда пишет статистические тесты на основе usage profiles. В прагматичной версии вы пишете property-based tests и просите коллегу их рецензировать.

from hypothesis import given, strategies as st

@given(
    capacity=st.integers(min_value=1, max_value=1000),
    initial=st.integers(min_value=0, max_value=1000),
    requests=st.lists(st.integers(min_value=1, max_value=100), max_size=50),
)
def test_token_bucket_never_overdrafts(capacity, initial, requests):
    bucket = TokenBucket(
        capacity=capacity,
        tokens=min(initial, capacity),
        refill_rate=0.0,
        last_refill=time.monotonic(),
    )

    for n in requests:
        granted = bucket.request(n)
        assert bucket.tokens >= 0
        if granted:
            # tokens were deducted, so pre-request balance was sufficient
            pass
        else:
            # request denied, current tokens insufficient
            assert bucket.tokens < n

Этот тест не проверяет конкретные outputs. Он проверяет инвариант: bucket никогда не выдаёт больше токенов, чем имеет. Это версия property-based доказательства Cleanroom. Он работает автоматически, находит edge cases, о которых вы не думали, и не требует отдельной команды верификации.

Компромиссы реальны

Прагматичный Cleanroom не бесплатен. Написание контрактов до кода требует дисциплины. Явные state machines кажутся boilerplate, когда код “очевиден”. Просить кого-то другого тестировать вашу логику требует координации.

Это также менее мощно, чем настоящая вещь. Правило no-execution в полном Cleanroom заставляет глубоко рассуждать, чего невозможно добиться, когда REPL находится в одном keystroke. Формальное доказательство ловит логические ошибки, которые property-based tests могут пропустить, если ваши properties неверны.

Но сравнение идёт не между прагматичным Cleanroom и полным Cleanroom. Сравнение идёт между прагматичным Cleanroom и тем, что вы делаете сейчас. Если ваш текущий процесс поставляет 20 дефектов на KLOC, а прагматичный Cleanroom снижает это до 5 — это улучшение в 4 раза за долю overhead.

Когда это стоит того

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

Сигнал о необходимости — не сложность. Это повторяющийся сюрприз. Если ваша команда постоянно находит одну и ту же категорию багов в тестах или продакшене, проблема не в небрежных разработчиках. Проблема в том, что контракт кода никогда не был определён, поэтому “корректность” никогда не была специфицирована.

Начните с одного модуля

Вам не нужно одобрение руководства или перестройка процесса. Выберите один модуль, который уже кусал вас раньше. Напишите его контракт в docstring, прежде чем трогать реализацию. Определите состояния и переходы. Попросите коллегу написать тесты, не глядя на ваш код. Запускайте property-based tests в CI.

Вот и всё. Никакой отдельной команды. Никакой формальной нотации. Никакого запрета на запуск собственного кода.

0,1 дефекта на KLOC от Cleanroom — это не магия. Это был результат процесса, который заставлял людей определять корректность до того, как её построить. Большую часть этого эффекта можно получить с помощью docstring, таблицы state machine и коллеги, который тестирует ваши предположения, а не ваш код.