La mayoría de los bugs se esconden en la brecha entre “lo que debería hacer” y “lo que realmente hace”
Escribes el código primero, luego los tests, y descubres que el código estaba mal. Ese es el loop estándar. Por eso el debugging consume la mitad de la mayoría de los timelines de proyecto.
Las Box Structures invierten esto. Defines el comportamiento antes de escribirlo, verificas esa definición matemáticamente, y luego la traduces a código capa por capa. El resultado es un module correcto por construcción, no correcto porque los tests pasaron por casualidad.
Suena imposible hasta que ves lo pequeña que es cada capa.
¿Qué es una Box Structure?
Una Box Structure describe un module de software en tres niveles de abstracción, cada uno un refinamiento estricto del anterior:
- Black box: ¿Qué estímulo produce qué respuesta? Sin estado. Sin implementación. Solo una función pura de historial a output.
- State box: ¿Qué estado recuerda el module, y cómo cada estímulo transforma ese estado y produce una respuesta?
- Clear box: El código real.
Diseñas de afuera hacia adentro. La black box es el contrato. La state box es el modelo de datos. La clear box es el código. En cada paso, demuestras que la capa inferior satisface la superior antes de continuar.
Esto no es documentación a posteriori. La black box y la state box son especificaciones formales. Son el diseño. El código viene al final.
La Black Box: El historial lo determina todo
Una black box define un module por su historial de estímulos y su respuesta. La respuesta a cualquier estímulo depende de cada estímulo anterior.
Considera un simple rate limiter de token bucket. La especificación de black box dice:
| 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 |
La black box no dice cómo se rastrean los tokens. Dice: dado este historial de estímulos, esta es la respuesta requerida.
Puedes verificar esto antes de que exista código. Escribe secuencias de estímulos, calcula las respuestas esperadas a mano, y verifica que la especificación se comporte correctamente. Sin compiler. Sin test runner. Solo lógica.
La State Box: Agregar memoria sin agregar suposiciones
La state box refina la black box introduciendo una variable de estado que hace el historial implícito. En lugar de cargar con el historial completo de estímulos, el module recuerda una representación comprimida.
Para el rate limiter, la state box introduce tokens, el número actual de tokens disponibles. La especificación se convierte en:
| 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 |
El paso crítico es demostrar que esta state box es equivalente a la black box. La variable de estado tokens debe representar fielmente el historial relevante. Si aplicar las reglas de la black box produce las mismas respuestas que el contador de la state box, el refinamiento es válido.
Esta prueba suele ser corta. Estás verificando una especificación de una página, no una codebase de mil líneas.
La Clear Box: Código que no puede sorprenderte
La clear box es la implementación. Se escribe en un lenguaje estructurado sin gotos ni flujo de control oculto. Toda clear box se construye a partir de secuencia, alternación (if-then-else) e iteración (while, for).
Aquí hay una implementación de clear box en 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)Observa que _refill no estaba en la state box. El tiempo no existe en la black box ni en la state box. Esos modelos asumen que los tokens aparecen por arte de magia cuando se llama a add_tokens. La clear box debe cerrar esa brecha.
Aquí es donde viven la mayoría de los bugs. La state box dice que tokens aumenta en k. La clear box también debe manejar el polyfill continuo y el límite de capacidad mientras sigue conforme a la state box.
Cómo Cleanroom demuestra corrección sin ejecutar tests
En Cleanroom, no escribes unit tests para la clear box. Realizas una verification.
Para cada estructura de control, escribes un predicado que debe cumplirse antes y después de su ejecución. Para una secuencia S1; S2, demuestras que la postcondición de S1 implica la precondición de S2. Para un if-then-else, demuestras que ambas branches satisfacen la postcondición general. Para un bucle while, encuentras un invariante y demuestras que se cumple al entrar, se preserva en cada iteración, e implica la postcondición deseada cuando el bucle termina.
Esto no es un proof assistant. Es lápiz y papel. Si alguna vez has argumentado informalmente que una función recursiva termina, ya has hecho el 90 por ciento de una prueba de Cleanroom.
Por qué la mayoría de los equipos no usa esto
La objeción obvia es tiempo. Escribir una black box, una state box y una prueba a mano suena más lento que simplemente escribir el código y arreglar los bugs.
Harlan Mills, quien desarrolló Cleanroom en IBM, midió lo contrario. Los equipos de Cleanroom entregaron código con un orden de magnitud menos defectos que los equipos de control, y su tiempo total de desarrollo fue menor porque casi no pasaron tiempo en el debugger.
La objeción menos obvia es cultural. Las Box Structures te obligan a pensar antes de escribir. La mayoría de los desarrolladores encuentran esto incómodo. La especificación se siente como burocracia. No lo es. Es el diseño. En Cleanroom, el diseño está escrito en una notación lo suficientemente precisa para verificar, no en un diagrama que el primer borrador de implementación ignora.
Cuándo las Box Structures valen el overhead
No necesitas especificar cada función de utilidad de esta manera. Las Box Structures brillan donde un bug cuesta más que el tiempo de escribir una especificación: payment processing, authorization, distributed consensus, protocols y workflow engines. También ayudan a equipos que envían repetidamente la misma categoría de bug a producción y nunca lo detectan en tests.
Una forma ligera de empezar
No necesitas adoptar el proceso completo de Cleanroom. Toma prestada la idea de Box Structure para un solo module.
Elige una función que haya causado problemas en producción. Escribe su black box: una tabla de inputs, conditions y expected outputs. No mires el código existente. Escribe lo que debería hacer, no lo que hace.
Luego escribe la state box. ¿Qué estado necesita? ¿Cómo cada input transforma ese estado? Compáralo con tu implementación. Donde difieran, has encontrado un bug o una suposición no documentada.
Aquí hay una plantilla mínima en Python que puedes 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)Los comentarios son la especificación. El código es la implementación. Mantenerlos en el mismo archivo hace que el refinamiento sea visible y revisable.
El verdadero valor es la separación de concerns
Las Box Structures no son magia. No atraparán todos los bugs. Lo que hacen es forzar una disciplina que la mayoría de los procesos de desarrollo omiten: definir qué significa correcto antes de construirlo.
La black box separa el contrato del module de sus internos. La state box separa el modelo de datos del código. La clear box separa la implementación de la prueba. Cada capa tiene un trabajo, y la verificas antes de pasar a la siguiente.
Por eso debería importarte. La brecha entre “lo que debería hacer” y “lo que hace” es donde viven tus bugs, y las Box Structures son una forma sistemática de cerrar esa brecha antes de escribir un solo test.
Si quieres profundizar, Cleanroom Software Engineering de Mills y los informes técnicos originales de IBM siguen siendo las referencias más claras. Las ideas son viejas. Los bugs que previenen, no.