A maioria dos bugs se esconde no gap entre “o que deveria fazer” e “o que realmente faz”
Você escreve o código primeiro, depois os testes, e descobre que o código estava errado. Esse é o loop padrão. É por isso que o debugging consome metade da timeline da maioria dos projetos.
As Box Structures invertem isso. Você define o comportamento antes de escrevê-lo, verifica essa definição matematicamente, e depois a traduz em código camada por camada. O resultado é um module correto por construção, não correto porque os testes passaram por acaso.
Isso soa impossível até você ver o quão pequena é cada camada.
O que é uma Box Structure?
Uma Box Structure descreve um module de software em três níveis de abstração, cada um um refinamento estrito do anterior:
- Black box: Que stimulus produz que response? Sem estado. Sem implementação. Apenas uma pure function do histórico para o output.
- State box: Que estado o module lembra, e como cada stimulus transforma esse estado e produz uma response?
- Clear box: O código real.
Você projeta de fora para dentro. A black box é o contrato. A state box é o data model. A clear box é o código. Em cada passo, você prova que a camada inferior satisfaz a camada superior antes de prosseguir.
Isso não é documentação posterior. A black box e a state box são especificações formais. Elas são o design. O código vem por último.
A Black Box: O histórico determina tudo
Uma black box define um module pelo seu histórico de stimuli e sua response. A response a qualquer stimulus depende de cada stimulus que veio antes.
Considere um simples rate limiter de token bucket. A especificação da black box diz:
| 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 |
A black box não diz como os tokens são rastreados. Ela diz: dado esse histórico de stimuli, essa é a response exigida.
Você pode verificar isso antes de qualquer código existir. Escreva sequências de stimuli, compute as responses esperadas à mão, e verifique se a especificação se comporta corretamente. Sem compiler. Sem test runner. Apenas lógica.
A State Box: Adicionar memória sem adicionar suposições
A state box refina a black box introduzindo uma variável de estado que torna o histórico implícito. Em vez de carregar o histórico completo de stimuli, o module lembra uma representação comprimida.
Para o rate limiter, a state box introduz tokens, o número atual de tokens disponíveis. A especificação torna-se:
| 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 |
O passo crítico é provar que essa state box é equivalente à black box. A variável de estado tokens deve representar fielmente o histórico relevante. Se aplicar as regras da black box produz as mesmas responses que o contador da state box, o refinamento é válido.
Essa prova geralmente é curta. Você está verificando uma especificação de uma página, não uma codebase de mil linhas.
A Clear Box: Código que não pode surpreender
A clear box é a implementação. É escrita em uma linguagem estruturada sem gotos e sem fluxo de controle oculto. Toda clear box é construída a partir de sequência, alternação (if-then-else) e iteração (while, for).
Aqui está uma implementação de clear box em 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)Note que _refill não estava na state box. O tempo não existe na black box ou na state box. Esses modelos assumem que os tokens aparecem magicamente quando add_tokens é chamado. A clear box deve preencher essa lacuna.
É aqui que a maioria dos bugs vive. A state box diz que tokens aumenta em k. A clear box também deve lidar com o reabastecimento contínuo e o limite de capacidade enquanto ainda permanece conforme à state box.
Como o Cleanroom prova correção sem executar testes
No Cleanroom, você não escreve unit tests para a clear box. Você realiza uma verification.
Para cada estrutura de controle, você escreve um predicado que deve valer antes e depois de sua execução. Para uma sequência S1; S2, você prova que a postcondição de S1 implica a pré-condição de S2. Para um if-then-else, você prova que ambos os branches satisfazem a postcondição geral. Para um loop while, você encontra um invariante e prova que ele vale na entrada, é preservado por cada iteração, e implica a postcondição desejada quando o loop termina.
Isso não é um proof assistant. É lápis e papel. Se você já argumentou informalmente que uma função recursiva termina, você já fez 90 por cento de uma prova de Cleanroom.
Por que a maioria das equipes não usa isso
A objeção óbvia é tempo. Escrever uma black box, uma state box e uma prova manual soa mais lento do que simplesmente escrever o código e consertar os bugs.
Harlan Mills, que desenvolveu o Cleanroom na IBM, mediu o oposto. As equipes de Cleanroom entregaram código com uma ordem de magnitude menos defeitos do que as equipes de controle, e seu tempo total de desenvolvimento foi menor porque gastaram quase nenhum tempo no debugger.
A objeção menos óbvia é cultural. As Box Structures forçam você a pensar antes de digitar. A maioria dos desenvolvedores acha isso desconfortável. A especificação parece burocracia. Não é. É o design. No Cleanroom, o design é escrito em uma notação precisa o suficiente para verificar, não em um diagrama que o primeiro rascunho de implementação ignora.
Quando as Box Structures valem o overhead
Você não precisa especificar cada função utilitária dessa forma. As Box Structures brilham onde um bug custa mais do que o tempo para escrever uma especificação: payment processing, authorization, distributed consensus, protocols e workflow engines. Elas também ajudam equipes que enviam repetidamente a mesma categoria de bug para produção e nunca a detectam nos testes.
Uma forma leve de começar
Você não precisa adotar o processo completo do Cleanroom. Pegue emprestada a ideia de Box Structure para um único module.
Escolha uma função que causou problemas em produção. Escreva sua black box: uma tabela de inputs, conditions e expected outputs. Não olhe para o código existente. Escreva o que ela deveria fazer, não o que faz.
Depois escreva a state box. De que estado ela precisa? Como cada input transforma esse estado? Compare com sua implementação. Onde diferirem, você encontrou um bug ou uma suposição não documentada.
Aqui está um template mínimo em Python que você pode adaptar:
"""
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)Os comentários são a especificação. O código é a implementação. Mantê-los no mesmo arquivo torna o refinamento visível e revisável.
O valor real é a separação de concerns
As Box Structures não são mágica. Elas não pegarão todos os bugs. O que fazem é impor uma disciplina que a maioria dos processos de desenvolvimento pula: definir o que significa correto antes de construí-lo.
A black box separa o contrato do module de seus internos. A state box separa o data model do código. A clear box separa a implementação da prova. Cada camada tem um trabalho, e você a verifica antes de passar para a próxima.
É por isso que você deveria se importar. O gap entre “o que deveria fazer” e “o que faz” é onde seus bugs vivem, e as Box Structures são uma forma sistemática de fechar esse gap antes de escrever um único teste.
Se quiser se aprofundar, Cleanroom Software Engineering de Mills e os relatórios técnicos originais da IBM ainda são as referências mais claras. As ideias são antigas. Os bugs que previnem, não.