Le fossé entre spécification et code, nid des bugs

Une affirmation refait surface régulièrement dans les cercles de théorie des langages de programmation : « une spécification suffisamment détaillée est indiscernable du code ». L'idée est provocante : la frontière entre décrire ce qu'un programme doit faire et le faire réellement serait plus mince qu'on ne le pense. Si votre spécification est assez précise pour lever toute ambiguïté, vous avez en pratique déjà écrit le programme.

Ce n'est pas qu'une question de philosophie. Cela a des conséquences concrètes sur la façon dont on construit les logiciels, sur le rôle des spécifications et sur la raison pour laquelle la plupart des bugs ne sont pas des erreurs de codage, mais des lacunes de spécification. Comprendre où la spécification s'arrête et où l'implémentation commence change la manière dont vous abordez les tests, les types et la correction.

D'où viennent réellement la plupart des bugs

Demandez à un développeur d'où viennent les bugs, il répondra généralement « le code ». Pourtant, les études sur les défauts logiciels montrent autre chose : la plupart des bugs naissent dans l'écart entre l'intention et l'implémentation. Le code fait correctement ce que le développeur lui a demandé. Simplement, ce qu'on lui a demandé était faux, parce que la spécification, formelle ou informelle, était ambiguë, incomplète ou mal comprise.

Un exemple classique : une spécification indique « le système doit gérer les requêtes concurrentes ». Que signifie « gérer » ? Les traiter dans l'ordre ? Simultanément ? Les mettre en file d'attente s'il y en a trop ? Et qu'est-ce que « trop » ? Que se passe-t-il pour les requêtes qui arrivent alors que la file est pleine ? Ces questions ne sont pas des détails d'implémentation, ce sont des lacunes de spécification. Et chaque question sans réponse est un bug potentiel, car le développeur y répondra implicitement dans son code, et sa réponse ne correspondra peut-être pas à ce qu'attendent les utilisateurs ou les autres développeurs.

Le spectre de la précision des spécifications

Les spécifications existent sur un spectre allant de l'informel au formel.

• Langage naturel. « Le système de connexion doit être sécurisé et convivial. » C'est à peine une spécification, plutôt un vœu pieux. Chaque mot est ambigu. Qu'est-ce que « sécurisé » ? Qu'est-ce que « convivial » ? Ce sont des jugements de valeur déguisés en exigences.
• Langage naturel structuré. « Lorsqu'un utilisateur saisit un mot de passe incorrect trois fois en 10 minutes, verrouiller le compte pendant 30 minutes. » Plus précis, mais encore ambigu. Un envoi vide compte-t-il comme « mot de passe incorrect » ? Les trois tentatives doivent-elles être consécutives ? La fenêtre de 10 minutes est-elle glissante ou fixe ?
• Signatures de types. authenticate(username: string, password: string) -> Result<User, AuthError>. Cela spécifie précisément l'interface de la fonction, mais rien sur son comportement. Vous connaissez la forme des entrées et des sorties, pas le lien entre les deux.
• Spécifications basées sur les propriétés. « Pour toute paire nom d'utilisateur-mot de passe valide dans la base, authenticate renvoie Ok(user) où user.username == username. » Cela contraint le comportement plus finement, à l'aide de quantificateurs logiques.
• Spécification formelle. Un modèle mathématique complet du comportement du système : chaque état, chaque transition, chaque invariant. À ce niveau, la spécification et l'implémentation sont presque la même chose.

Plus on se rapproche de la spécification formelle, moins l'ambiguïté a de place, et moins les bugs en ont. Mais chaque étape demande aussi plus d'efforts et des compétences plus spécialisées. La question pratique est donc : jusqu'où aller sur ce spectre pour un projet donné ?

Les types comme spécifications légères

Les systèmes de types sont la forme de spécification la plus répandue dans la programmation quotidienne. Ils ne décrivent pas le comportement, mais ils le contraignent. Une fonction qui renvoie Option<User> au lieu de User indique qu'elle peut ne pas trouver d'utilisateur, et le compilateur oblige chaque appelant à gérer ce cas.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

Des langages comme Rust, Haskell ou TypeScript montrent comment des systèmes de types expressifs réduisent l'écart de spécification sans exiger de formation aux méthodes formelles. Les types algébriques, les contraintes génériques et le pattern matching exhaustif spécifient collectivement une bonne partie du comportement du programme au niveau des types, et le compilateur le vérifie automatiquement.

L'idée clé : chaque annotation de type est une spécification qui est vérifiée automatiquement. Chaque comportement que vous pouvez encoder dans le système de types est une classe de bugs que vous n'aurez jamais.

Tests basés sur les propriétés : spécifier le comportement

Les tests unitaires sont des spécifications par l'exemple : « pour cette entrée précise, attendre cette sortie précise ». Ils sont utiles, mais intrinsèquement incomplets, car on ne peut tester que les cas auxquels on pense. Les tests basés sur les propriétés inversent cette logique : on spécifie les propriétés qui doivent être vraies pour toutes les entrées, et le framework de test génère des entrées aléatoires pour trouver les violations.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

Les trois propriétés de ce test ne se contentent pas de tester le tri : elles le définissent. Toute fonction qui satisfait ces trois propriétés est, par définition, un tri correct. C'est l'idée de « spécification comme code » sous sa forme la plus concrète : on écrit des propriétés qui définissent le comportement correct, puis on laisse le framework vérifier que l'implémentation les satisfait.

TLA+ et model checking

Pour les systèmes où les bugs coûtent cher (systèmes distribués, plateformes financières, infrastructures critiques), des outils de spécification formelle comme TLA+ offrent des garanties plus fortes. TLA+ (Temporal Logic of Actions) permet de décrire le comportement d'un système sous forme de machine à états, puis de le vérifier par model checking : explorer exhaustivement toutes les exécutions possibles pour vérifier que les invariants tiennent.

Amazon a utilisé TLA+ pour vérifier des algorithmes de S3, DynamoDB et d'autres services critiques d'AWS. L'entreprise a publiquement décrit des bugs qu'il aurait été quasiment impossible de trouver par les tests, des bugs qui n'apparaissent que sous certains entrelacements d'opérations concurrentes, qui ne surviennent qu'une fois sur des millions d'exécutions.

La spécification TLA+ d'un protocole de consensus comme Raft fait généralement quelques centaines de lignes. Elle décrit chaque transition d'état légale, chaque invariant (par exemple « au plus un leader par mandat ») et chaque propriété de sûreté. Le model checker explore ensuite des milliards de chemins d'exécution possibles et vérifie qu'aucun ne viole un invariant. C'est une spécification réellement proche du code, suffisamment précise pour être traduite mécaniquement en implémentation.

Conception par contrat

La Conception par contrat (Design by Contract, DbC) de Bertrand Meyer occupe un terrain intermédiaire et pragmatique. Chaque fonction spécifie des préconditions (ce qui doit être vrai avant l'appel), des postconditions (ce que la fonction garantit au retour) et des invariants (ce qui doit toujours être vrai pour l'objet). Ces contrats sont vérifiés à l'exécution pendant le développement, et peuvent être désactivés en production pour des raisons de performance.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

La postcondition de conservation, selon laquelle le total d'argent avant et après le transfert est identique, est exactement le type d'invariant qui détecte des bugs que les tests unitaires couvrent rarement. Elle spécifie une propriété fondamentale du système (l'argent ne se crée ni ne se détruit) que toute implémentation correcte doit satisfaire.

Recommandations pratiques

Une spécification formelle complète n'est pas réaliste pour la plupart des logiciels. Mais vous pouvez réduire fortement l'écart de spécification avec des techniques qui s'intègrent dans un flux de développement normal.

1. Utilisez agressivement le système de types. Encodez les contraintes sous forme de types dès que possible. Préférez NonEmptyList à List quand la liste ne doit pas être vide. Utilisez des wrappers newtype pour distinguer UserId de OrderId, même si ce sont tous deux des chaînes. Chaque contrainte encodée dans les types est une contrainte que le compilateur vérifie gratuitement.
2. Écrivez des tests basés sur les propriétés pour la logique cœur. Identifiez les invariants que votre système doit maintenir et exprimez-les sous forme de tests de propriétés. Quelques propriétés bien choisies détectent des bugs que des milliers de tests par l'exemple laissent passer.
3. Spécifiez les frontières. Les spécifications les plus importantes se situent aux frontières du système : contrats d'API, schémas de base de données, formats de messages. Utilisez OpenAPI, Protocol Buffers ou JSON Schema pour les rendre vérifiables par machine.
4. Utilisez TLA+ ou Alloy pour les systèmes concurrents critiques. Si vous concevez un algorithme de consensus, un verrou distribué ou un système de transactions financières, le coût d'une spécification formelle est faible comparé à celui des bugs de correction subtils en production.
5. Écrivez votre spec avant vos tests. Si vous ne pouvez pas dire précisément à quoi ressemble un comportement correct, vous ne pouvez pas le vérifier. Passer 30 minutes à rédiger une spécification claire de ce que doit faire une fonction (tous les cas, y compris les cas limites) révèle souvent des problèmes de conception avant même d'écrire la moindre ligne de code.

L'affirmation selon laquelle « une spec suffisamment détaillée est du code » n'est pas tout à fait juste. Il est plus exact de dire qu'une spec suffisamment détaillée supprime la place des bugs. L'écart entre spécification et implémentation est là où vit l'ambiguïté, et l'ambiguïté est le terreau des bugs. Chaque technique qui réduit cet écart (types, propriétés, contrats, méthodes formelles) rend votre logiciel plus correct. Non pas parce qu'elle empêche les erreurs de codage, mais parce qu'elle empêche les erreurs de spécification dont proviennent habituellement les erreurs de codage.