Découvrez comment les travaux de Tony Hoare — logique de Hoare, Quicksort et une mentalité orientée sécurité — ont façonné des techniques pratiques pour écrire et relire du logiciel correct.
Quand on dit qu’un programme est « correct », on entend souvent : « Je l’ai exécuté quelques fois et la sortie avait l’air bonne. » C’est un signal utile — mais ce n’est pas la correction. En termes simples, la correction signifie que le programme respecte sa spécification : pour chaque entrée autorisée, il produit le résultat requis et respecte les règles sur les changements d’état, le temps et les erreurs.
Le piège est que « respecter sa spec » est plus difficile qu’on ne le pense.
D’abord, les spécifications sont souvent ambiguës. Une exigence produit peut dire « trier la liste », mais veut‑on un tri stable ? Qu’en est‑il des valeurs dupliquées, des listes vides ou d’éléments non numériques ? Si la spec ne le précise pas, différentes personnes en déduiront des choses différentes.
Ensuite, les cas limites ne sont pas rares — ils sont juste moins testés. Valeurs nulles, dépassement d’entier, décalages d’un (off‑by‑one), séquences d’utilisateur inhabituelles et pannes externes inattendues peuvent transformer un « ça a l’air de marcher » en « ça a planté en production ».
Enfin, les exigences changent. Un programme peut être correct par rapport à la spec d’hier et incorrect par rapport à celle d’aujourd’hui.
La grande contribution de Tony Hoare n’était pas la revendication qu’il faille tout prouver tout le temps. C’était l’idée que nous pouvons être plus précis sur ce que le code doit faire — et le raisonner de manière disciplinée.
Dans ce billet, nous suivrons trois fils connectés :
La plupart des équipes n’écriront pas de preuves formelles complètes. Mais même une pensée « à la manière d’une preuve » partielle peut rendre les bugs plus faciles à repérer, améliorer la qualité des revues et clarifier le comportement avant la livraison.
Tony Hoare est un de ces rares informaticiens dont le travail n’est pas resté cantonné aux articles ou aux salles de cours. Il a navigué entre université et industrie, et il se souciait d’une question pratique que chaque équipe rencontre encore : comment savoir qu’un programme fait bien ce qu’on pense qu’il fait — surtout lorsque les enjeux sont élevés ?
Cet article se concentre sur quelques idées de Hoare qui reviennent dans les bases de code réelles :
{P} C {Q}.Vous ne trouverez pas ici un formalisme mathématique poussé, et nous n’allons pas tenter une preuve complète et vérifiée par machine de Quicksort. L’objectif est de garder les concepts accessibles : assez de structure pour clarifier votre raisonnement, sans transformer votre revue de code en séminaire de doctorat.
Les idées de Hoare se traduisent en décisions ordinaires : sur quelles hypothèses une fonction compte, ce qu’elle garantit aux appelants, ce qui doit rester vrai à mi‑boucle, et comment repérer des changements « presque corrects » pendant les revues. Même quand vous n’écrivez jamais explicitement {P} C {Q}, penser dans cette forme améliore les API, les tests et la qualité des discussions autour du code délicat.
La vision de Hoare est plus stricte que « ça a passé quelques exemples » : la correction, c’est tenir une promesse convenue, pas seulement paraître juste sur un petit échantillon.
Les bugs surviennent souvent quand les équipes sautent l’étape du milieu : elles vont des exigences directement au code, laissant la « promesse » floue.
Deux affirmations différentes sont souvent confondues :
Pour les systèmes réels, « ne jamais finir » peut être aussi dommageable que « finir avec la mauvaise réponse ».
Les énoncés de correction ne sont jamais universels ; ils reposent sur des hypothèses concernant :
Rendre les hypothèses explicites transforme un « ça marche sur ma machine » en quelque chose dont d’autres peuvent raisonner.
Considérons une fonction sortedCopy(xs).
Une spec utile pourrait être : « Retourne une nouvelle liste ys telle que (1) ys est triée en ordre croissant, et (2) ys contient exactement les mêmes éléments que xs (mêmes occurrences), et (3) xs reste inchangée. »
Maintenant, « correct » signifie que le code satisfait ces trois points sous les hypothèses énoncées — pas seulement que la sortie a l’air triée lors d’un test rapide.
La logique de Hoare est une manière de parler du code avec la même clarté que pour un contrat : si vous commencez dans un état qui satisfait certaines hypothèses, et que vous exécutez ce fragment de code, vous finirez dans un état qui satisfait certaines garanties.
La notation centrale est le triplet de Hoare :
{precondition} program {postcondition}
Une précondition énonce ce qui doit être vrai avant l’exécution du fragment. Il ne s’agit pas de ce que vous espérez ; c’est ce dont le code a besoin.
Exemple : supposons une fonction qui retourne la moyenne de deux nombres sans vérification de dépassement.
a + b tient dans le type entieravg = (a + b) / 2avg vaut la moyenne mathématique de a et bSi la précondition ne tient pas (dépassement possible), la promesse de la postcondition ne s’applique plus. Le triplet vous oblige à le dire à voix haute.
Une postcondition indique ce qui sera vrai après l’exécution — en supposant que la précondition était satisfaite. De bonnes postconditions sont concrètes et vérifiables. Au lieu de « résultat valide », dites ce que « valide » signifie : trié, non négatif, dans les bornes, inchangé sauf certains champs, etc.
La logique de Hoare s’applique des opérations élémentaires aux blocs multi‑étapes :
x = x + 1, quelles propriétés sur x sont maintenant vraies ?Le but n’est pas d’astiquer votre code de triplets partout. C’est de rendre l’intention lisible : hypothèses claires, résultats clairs, et moins de conversations « ça a l’air de marcher » pendant les revues.
Un invariant de boucle est une affirmation vraie avant que la boucle ne commence, qui reste vraie après chaque itération, et qui est encore vraie quand la boucle se termine. C’est une idée simple avec un grand bénéfice : elle remplace le « ça a l’air de marcher » par une revendication que vous pouvez réellement vérifier à chaque étape.
Sans invariant, une revue ressemble souvent à : « On itère sur la liste et on corrige progressivement des choses. » Un invariant force la précision : qu’est‑ce qui est déjà correct maintenant, même si la boucle n’est pas finie ? Une fois que vous pouvez le dire clairement, les erreurs d’un décalage et les cas manquants deviennent plus faciles à repérer, car ils apparaissent comme des moments où l’invariant serait violé.
La plupart du code quotidien peut réutiliser quelques modèles fiables.
Garder les indices dans une plage sûre.
0 <= i <= nlow <= left <= right <= highCe type d’invariant empêche les accès hors plage et rend le raisonnement sur les tableaux concret.
Divisez vos données en une région « faite » et une région « pas encore ».
a[0..i) ont été examinés. »result satisfait le prédicat de filtrage. »Cela transforme le progrès vague en contrat clair sur ce que « traité » signifie.
Commun dans le tri, le merge et la partition.
a[0..i) est trié. »a[0..i) sont <= pivot, et tous les éléments dans a[j..n) sont >= pivot. »Même si le tableau complet n’est pas encore trié, vous avez défini précisément ce qui l’est.
La correction n’est pas seulement d’avoir raison ; la boucle doit aussi se terminer. Une façon simple d’argumenter est de nommer une mesure (ou variant) qui diminue à chaque itération et ne peut pas diminuer indéfiniment.
Exemples :
n - i diminue de 1 à chaque fois. »Si vous ne trouvez pas de mesure qui décroît, vous avez peut‑être découvert un risque réel : une boucle infinie sur certains inputs.
Quicksort a une promesse simple : donné un segment de tableau, réarranger ses éléments pour qu’ils soient en ordre non décroissant, sans perdre ni inventer de valeurs. La forme haute‑niveau de l’algorithme est facile à résumer :
C’est un excellent exemple pédagogique pour la correction car il est assez petit pour être compris, mais suffisamment riche pour montrer où le raisonnement informel échoue. Un Quicksort qui « a l’air de marcher » sur quelques tests aléatoires peut quand même être incorrect sur des entrées spécifiques ou des conditions limites.
Quelques problèmes provoquent la plupart des bugs :
Pour raisonner en style Hoare, on sépare typiquement la preuve en deux parties :
Cette séparation rend le raisonnement gérable : corrigez la partition, puis construisez la correction du tri sur cette base.
La rapidité de Quicksort dépend d’une routine apparemment petite : la partition. Si la partition est légèrement fausse, Quicksort peut mal trier, boucler indéfiniment ou planter sur des cas limites.
Nous utiliserons le schéma classique de partition de Hoare (deux pointeurs se déplaçant vers l’intérieur).
Entrée : une tranche de tableau A[lo..hi] et une valeur pivot choisie (souvent A[lo]).
Sortie : un indice p tel que :
A[lo..p] est <= pivotA[p+1..hi] est >= pivotRemarquez ce qui n’est pas promis : le pivot n’est pas forcément à la position p, et les éléments égaux au pivot peuvent apparaître de part et d’autre. C’est acceptable — Quicksort a seulement besoin d’une séparation correcte.
Tandis que l’algorithme avance deux indices — i depuis la gauche et j depuis la droite — un bon raisonnement se concentre sur ce qui est déjà « verrouillé ». Un ensemble pratique d’invariants est :
A[lo..i-1] sont <= pivot (le côté gauche est propre)A[j+1..hi] sont >= pivot (le côté droit est propre)A[i..j] est non classé (à vérifier)Lorsque l’on trouve A[i] >= pivot et A[j] <= pivot, les échanger préserve ces invariants et rétrécit le milieu non classé.
i va jusqu’à droite ; la partition doit malgré tout terminer et renvoyer un p sensé.j va vers la gauche ; même souci de terminaison.< vs <=), les pointeurs peuvent se bloquer. Le schéma de Hoare repose sur une règle cohérente pour assurer le progrès.Il existe différents schémas de partition (Lomuto, Hoare, partition à trois voies). L’essentiel est d’en choisir un, d’énoncer son contrat, et de revoir le code par rapport à ce contrat de manière cohérente.
La récursion est plus facile à faire confiance quand on peut répondre à deux questions clairement : quand s’arrête‑t‑elle ? et pourquoi chaque étape est‑elle valide ? La pensée à la manière de Hoare aide car elle vous oblige à énoncer ce qui doit être vrai avant un appel, et ce qui sera vrai après son retour.
Une fonction récursive a besoin d’au moins un cas de base où elle n’effectue plus d’appels récursifs et satisfait quand même le résultat promis.
Pour le tri, un cas de base typique est « les tableaux de longueur 0 ou 1 sont déjà triés ». Ici, « trié » doit être explicite : pour une relation d’ordre ≤, le tableau de sortie est trié si pour tout indice i < j, on a a[i] ≤ a[j]. (La conservation de l’ordre des éléments égaux est une propriété distincte appelée stabilité ; Quicksort n’est pas stable à moins d’être conçu pour l’être.)
Chaque étape récursive doit appeler la fonction sur une entrée strictement plus petite. Ce « rétrécissement » est l’argument de terminaison : si la taille diminue et ne peut pas descendre en dessous de 0, on ne peut pas récuser indéfiniment.
Le rétrécissement importe aussi pour la sécurité de la pile. Même un code correct peut planter si la profondeur de récursion devient trop grande. Dans Quicksort, des partitions déséquilibrées peuvent créer une récursion profonde. C’est un argument de terminaison et un rappel pratique de considérer la profondeur maximale.
Le pire cas de Quicksort est O(n²) lorsque les partitions sont très déséquilibrées, mais c’est un problème de performance — pas de correction. L’objectif du raisonnement est : en supposant que la partition préserve les éléments et les sépare selon le pivot, le tri récursif des sous‑plages implique que l’ensemble devient trié selon la définition de tri.
Tests et raisonnement visent la même chose — la confiance — mais par des voies différentes.
Les tests sont excellents pour attraper des erreurs concrètes : un off‑by‑one, un cas limite manquant, une régression. Mais une suite de tests ne peut qu’échantillonner l’espace d’entrée. Même une « couverture à 100% » n’implique pas que tous les comportements ont été vérifiés ; cela signifie surtout que toutes les lignes ont été exécutées.
Le raisonnement en style preuve (en particulier la logique de Hoare) part d’une spécification et demande : si ces préconditions tiennent, le code établit‑il toujours les postconditions ? Bien fait, vous n’éliminez pas seulement un bug — vous pouvez souvent écarter une catégorie entière de bugs (comme « accès hors bornes » ou « la boucle ne casse pas la propriété de partition »).
Une spec claire est un générateur de tests.
Si votre postcondition dit « la sortie est triée et est une permutation de l’entrée », vous obtenez automatiquement des idées de tests :
La spec vous dit ce que « correct » signifie, et les tests vérifient que la réalité s’y conforme.
Les tests basés sur les propriétés se placent entre les preuves et les exemples. Au lieu de choisir quelques cas, on énonce des propriétés et on laisse un outil générer beaucoup d’entrées.
Pour le tri, deux propriétés simples suffisent souvent :
Ces propriétés sont essentiellement des postconditions écrites comme vérifications exécutables.
Une routine légère qui s’échelonne :
Si vous voulez institucionaliser cela, faites de la « spec + notes de raisonnement + tests » une partie de votre template de PR ou de votre checklist de revue de code (voir aussi /blog/code-review-checklist).
Si vous utilisez un flux de travail génératif (génération de code à partir d’une interface chat), la même discipline s’applique — peut‑être davantage. Sur Koder.ai, par exemple, on peut commencer en mode Planning pour fixer des préconditions/postconditions avant toute génération de code, puis itérer avec snapshots et rollback tout en ajoutant des tests basés sur les propriétés. L’outil accélère l’implémentation, mais la spec reste ce qui empêche le « rapide » de devenir « fragile ».
La correction ne se réduit pas à « le programme renvoie la bonne valeur ». La pensée sécurité pose une autre question : quels résultats sont inacceptables, et comment les prévenir — même quand le code est mis à l’épreuve, mal utilisé ou partiellement défaillant ? En pratique, la sécurité, c’est la correction avec un système de priorités : certains échecs sont seulement gênants, d’autres peuvent causer des pertes financières, des fuites de données ou des dommages physiques.
Un bug est un défaut dans le code ou la conception. Un hazard (danger) est une situation pouvant conduire à un résultat inacceptable. Un bug peut être inoffensif dans un contexte et dangereux dans un autre.
Exemple : un off‑by‑one dans une galerie photo peut mal étiqueter une image ; la même erreur dans un calculateur de dosage médicamenteux peut blesser un patient. La pensée sécurité vous force à relier le comportement du code aux conséquences, pas seulement à la conformité à la spec.
Pas besoin de méthodes formelles lourdes pour obtenir des gains immédiats en sécurité. Les équipes peuvent adopter des pratiques petites et répétables :
Ces techniques s’accordent bien avec la logique de Hoare : explicitez les préconditions (entrées acceptables) et incluez des propriétés de sécurité dans les postconditions (ce qui ne doit jamais arriver).
Les checks orientés sécurité coûtent en CPU, en complexité ou en refus de faux positifs occasionnels.
La pensée sécurité vise moins l’élégance que la prévention des modes d’échec que l’on ne peut pas se permettre.
Les revues de code sont l’endroit où la pensée correction paye le plus vite, car vous pouvez repérer des hypothèses manquantes bien avant que les bugs n’atteignent la production. L’idée centrale de Hoare — énoncer ce qui doit être vrai avant et ce qui sera vrai après — se traduit directement en questions de revue.
Quand vous lisez un changement, essayez d’encadrer chaque fonction clé comme une petite promesse :
Une habitude simple pour le relecteur : si vous ne pouvez pas dire les pré/post conds en une phrase, le code a probablement besoin d’une structure plus claire.
Pour les fonctions risquées ou centrales, ajoutez un petit commentaire‑contrat au‑dessus de la signature. Restez concret : entrées, sorties, effets et erreurs.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Ces commentaires ne sont pas des preuves formelles, mais ils donnent aux relecteurs quelque chose de précis à vérifier.
Soyez explicite en revoyant du code qui gère :
Si la modification touche l’un de ces domaines, demandez : « Quelles sont les préconditions, et où sont‑elles appliquées ? » et « Quelles garanties fournissons‑nous même en cas d’erreur ? »
Le raisonnement formel ne signifie pas forcément transformer toute votre base de code en article mathématique. L’objectif est d’investir plus de certitude là où ça paye : endroits où « ça a l’air correct dans les tests » n’est pas suffisant.
Elles conviennent bien quand vous avez un module petit et critique dont tout dépend (auth, règles de paiement, permissions, verrous de sécurité), ou un algorithme délicat où des off‑by‑one se cachent longtemps (parseurs, ordonnancement, cache/éviction, primitives concurrentes, code de partition, transformations riches en frontières).
Une règle utile : si un bug peut causer dommage réel, grosse perte financière ou corruption silencieuse de données, vous voulez plus que la revue ordinaire + tests.
Vous pouvez choisir entre « léger » et « lourd », et souvent le meilleur résultat vient d’une combinaison :
Décidez du degré de formalisme en pesant :
En pratique, vous pouvez aussi voir la « formalité » comme un ajout progressif : commencez par des contrats explicites et invariants, puis laissez l’automatisation vérifier cela. Pour des équipes qui itèrent vite (par ex. avec Koder.ai — génération d’un front React, d’un backend Go et d’un schéma Postgres en boucle), les snapshots/rollbacks et l’export de code facilitent d’itérer rapidement tout en appliquant des contrats via tests et analyse statique dans la CI.
Utilisez‑la comme un gate « faut‑il formaliser davantage ? » en planification ou en revue :
Lectures complémentaires : design-by-contract, tests basés sur les propriétés, model checking pour machines d’état, analyse statique pour votre langage, et matériaux d’introduction aux assistants de preuve et aux spécifications formelles.
La correction désigne le fait qu’un programme respecte une spécification convenue : pour chaque entrée autorisée et pour les états système pertinents, il produit les sorties et effets secondaires attendus (et gère les erreurs comme prévu). « Ça a l’air de marcher » signifie généralement que vous n’avez vérifié que quelques exemples, pas tout l’espace d’entrées ni les conditions limites problématiques.
Les bugs surviennent souvent quand on saute l’étape intermédiaire : on va des requirements directement au code, en laissant la « promesse » floue.
En pratique, la correction totale importe chaque fois qu’un « blocage » visible par l’utilisateur, une fuite de ressources ou un risque de sécurité est inacceptable.
Un triplet de Hoare {P} C {Q} se lit comme un contrat :
P (précondition) : ce qui doit être vrai avant d’exécuter CLes préconditions sont ce dont le code a besoin (par ex. « les indices sont dans les limites », « les éléments sont comparables », « le verrou est acquis »).
Si une précondition peut être violée par les appelants, il faut soit :
Sinon, vos postconditions deviennent de l’optimisme.
Un invariant de boucle est une affirmation vraie avant le début de la boucle, qui reste vraie après chaque itération et est encore vraie à la fin de la boucle. Modèles réutilisables :
0 <= i <= n)Si vous ne pouvez pas énoncer un invariant, c’est souvent le signe que la boucle fait trop de choses ou que ses bornes sont confuses.
On nomme une mesure (variant) qui décroît à chaque itération et ne peut pas décroître indéfiniment, par exemple :
n - i qui décroît de 1Si vous ne trouvez pas de mesure décroissante, vous avez peut‑être découvert un vrai risque de non-terminaison (pointeurs bloqués, duplicats mal gérés).
La partition est la petite routine dont dépend tout Quicksort. Si la partition est un peu fausse, vous pouvez obtenir :
D’où l’importance d’énoncer explicitement le contrat de partition : ce qui doit être vrai à gauche, à droite, et que les éléments sont simplement réarrangés (permutation).
Les doublons et le traitement des éléments « égaux au pivot » sont des points d’échec fréquents. Règles pratiques :
i/j bloqué)Si les doublons sont fréquents, la partition à trois voies réduit à la fois les bugs et la profondeur de récursion.
Les tests trouvent des erreurs concrètes ; le raisonnement en style preuve élimine des classes entières de bugs (sécurité des bornes, préservation d’invariants, terminaison). Un flux de travail hybride utile :
Pour le tri, deux propriétés de haute valeur : tri (ordre non décroissant) et permutation (mêmes éléments, mêmes comptes).
CQ (postcondition) : ce qui sera vrai après l’exécution de C, en supposant que P était vraiVous n’avez pas besoin d’écrire la notation dans le code : utiliser la même structure dans les revues (« hypothèses entrantes, garanties sortantes ») est le gain pratique.