La plupart des bugs se cachent dans l’écart entre “ce qu’il devrait faire” et “ce qu’il fait réellement”
Vous écrivez d’abord le code, puis les tests, puis vous découvrez que le code était faux. C’est la boucle standard. C’est aussi pourquoi le debugging consomme la moitié de la plupart des timelines de projet.
Les Box Structures inversent cela. Vous définissez le comportement avant de l’écrire, vous vérifiez cette définition mathématiquement, puis vous la traduisez en code couche par couche. Le résultat est un module correct par construction, pas correct parce que les tests ont passé par hasard.
Cela semble impossible jusqu’à ce qu’on voie à quel point chaque couche est petite.
Qu’est-ce qu’une Box Structure ?
Une Box Structure décrit un module logiciel à trois niveaux d’abstraction, chacun étant un raffinement strict du précédent :
- Black box : Quel stimulus produit quelle réponse ? Pas d’état. Pas d’implémentation. Juste une fonction pure de l’historique vers la sortie.
- State box : Quel état le module mémorise-t-il, et comment chaque stimulus transforme-t-il cet état et produit-il une réponse ?
- Clear box : Le code réel.
Vous concevez de l’extérieur vers l’intérieur. La black box est le contrat. La state box est le modèle de données. La clear box est le code. À chaque étape, vous prouvez que la couche inférieure satisfait la couche supérieure avant de passer à la suite.
Ce n’est pas de la documentation a posteriori. La black box et la state box sont des spécifications formelles. Ce sont la conception. Le code vient en dernier.
La Black Box : L’historique détermine tout
Une black box définit un module par son historique de stimuli et sa réponse. La réponse à un stimulus dépend de chaque stimulus qui l’a précédé.
Prenons un simple rate limiter de type token bucket. La spécification de la black box dit :
| 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 ne dit pas comment les tokens sont suivis. Elle dit : étant donné cet historique de stimuli, voici la réponse requise.
Vous pouvez vérifier cela avant qu’aucun code n’existe. Écrivez des séquences de stimuli, calculez les réponses attendues à la main, et vérifiez que la spécification se comporte correctement. Pas de compilateur. Pas de test runner. Juste de la logique.
La State Box : Ajouter de la mémoire sans ajouter d’hypothèses
La state box affine la black box en introduisant une variable d’état qui rend l’historique implicite. Au lieu de traîner l’historique complet des stimuli, le module se souvient d’une représentation compressée.
Pour le rate limiter, la state box introduit tokens, le nombre actuel de tokens disponibles. La spécification devient :
| 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 |
L’étape critique consiste à prouver que cette state box est équivalente à la black box. La variable d’état tokens doit représenter fidèlement l’historique pertinent. Si l’application des règles de la black box produit les mêmes réponses que le compteur de la state box, le raffinement est valide.
Cette preuve est généralement courte. Vous vérifiez une spécification d’une page, pas une codebase de mille lignes.
La Clear Box : Du code qui ne peut pas vous surprendre
La clear box est l’implémentation. Elle est écrite dans un langage structuré sans goto et sans flux de contrôle caché. Chaque clear box est construite à partir de séquence, d’alternation (if-then-else) et d’itération (while, for).
Voici une implémentation 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)Notez que _refill n’était pas dans la state box. Le temps n’existe pas dans la black box ou la state box. Ces modèles supposent que les tokens apparaissent par magie quand add_tokens est appelé. La clear box doit combler cet écart.
C’est ici que vivent la plupart des bugs. La state box dit que tokens augmente de k. La clear box doit aussi gérer le remplissage continu et la limite de capacité tout en restant conforme à la state box.
Comment Cleanroom prouve la correction sans exécuter de tests
Dans Cleanroom, vous n’écrivez pas de unit tests pour la clear box. Vous effectuez une verification.
Pour chaque structure de contrôle, vous écrivez un prédicat qui doit être vrai avant et après son exécution. Pour une séquence S1; S2, vous prouvez que la postcondition de S1 implique la precondition de S2. Pour un if-then-else, vous prouvez que les deux branches satisfont la postcondition globale. Pour une boucle while, vous trouvez un invariant et prouvez qu’il est vrai à l’entrée, préservé à chaque itération, et qu’il implique la postcondition désirée quand la boucle se termine.
Ce n’est pas un proof assistant. C’est papier et crayon. Si vous avez déjà argumenté informellement qu’une fonction récursive termine, vous avez déjà fait 90 pour cent d’une preuve Cleanroom.
Pourquoi la plupart des équipes n’utilisent pas cela
L’objection évidente est le temps. Écrire une black box, une state box et une preuve à la main semble plus lent que simplement écrire le code et corriger les bugs.
Harlan Mills, qui a développé Cleanroom chez IBM, a mesuré le contraire. Les équipes Cleanroom ont livré du code avec un ordre de grandeur moins de défauts que les équipes témoins, et leur temps de développement total était plus court car ils passaient presque pas de temps dans le debugger.
L’objection moins évidente est culturelle. Les Box Structures vous obligent à réfléchir avant de taper. La plupart des développeurs trouvent cela inconfortable. La spécification ressemble à de la bureaucratie. Ce n’en est pas. C’est la conception. Dans Cleanroom, la conception est écrite dans une notation assez précise pour être vérifiée, pas dans un diagramme que le premier brouillon d’implémentation ignore.
Quand les Box Structures valent le surcoût
Vous n’avez pas besoin de spécifier chaque fonction utilitaire de cette façon. Les Box Structures brillent là où un bug coûte plus cher que le temps d’écrire une spécification : payment processing, authorization, distributed consensus, protocoles et workflow engines. Elles aident aussi les équipes qui envoient répétitivement la même catégorie de bug en production et ne la détectent jamais dans les tests.
Une manière légère de commencer
Vous n’avez pas besoin d’adopter le processus Cleanroom complet. Empruntez l’idée de Box Structure pour un seul module.
Choisissez une fonction qui a causé des problèmes en production. Écrivez sa black box : un tableau d’inputs, de conditions et d’expected outputs. Ne regardez pas le code existant. Écrivez ce qu’elle devrait faire, pas ce qu’elle fait.
Puis écrivez la state box. De quel état a-t-elle besoin ? Comment chaque input transforme-t-il cet état ? Comparez-la à votre implémentation. Là où elles diffèrent, vous avez trouvé un bug ou une assumption non documentée.
Voici un template minimal en Python que vous pouvez adapter :
"""
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)Les commentaires sont la spécification. Le code est l’implémentation. Les garder dans le même fichier rend le raffinement visible et reviewable.
La vraie valeur est la separation of concerns
Les Box Structures ne sont pas magiques. Elles n’attraperont pas tous les bugs. Ce qu’elles font, c’est imposer une discipline que la plupart des processus de développement ignorent : définir ce que correct signifie avant de le construire.
La black box sépare le contrat du module de ses internals. La state box sépare le modèle de données du code. La clear box sépare l’implémentation de la preuve. Chaque couche a un seul travail, et vous la vérifiez avant de passer à la suivante.
C’est pourquoi cela devrait vous importer. L’écart entre “ce qu’il devrait faire” et “ce qu’il fait” est là où vivent vos bugs, et les Box Structures sont une méthode systématique pour combler cet écart avant d’écrire un seul test.
Si vous voulez aller plus loin, Cleanroom Software Engineering de Mills et les rapports techniques originaux d’IBM restent les références les plus claires. Les idées sont vieilles. Les bugs qu’elles préviennent, non.