Le 4 juin 1996, le vol inaugural d'Ariane 5 est détruit 37 secondes…

La borne. Sur $16$ bits signés, les valeurs vont de $-32768$ à $2^{15}-1=32767$.

La conversion. Une mesure valant $32768$ ne rentre pas. Réduite modulo $2^{16}$ puis relue en complément à deux, elle donne $-32768$ : plus_n_bits(32767, 1, 16) rend bien $-32768$. Une vitesse positive devient une vitesse négative — et rien ne le signale.

Ce qui s'est réellement passé. Le code venait d'Ariane 4, où cette conversion était sûre : la trajectoire d'Ariane 4 ne produisait jamais une valeur aussi grande. La précondition implicite « la vitesse horizontale reste inférieure à $32767$ » était vraie pour Ariane 4, fausse pour Ariane 5, plus rapide. Elle n'était écrite nulle part.

La leçon. Une précondition non écrite est une précondition non vérifiée. Réemployer un code correct dans un contexte différent, c'est réemployer ses préconditions — et celles-ci ne voyagent pas toutes seules. Le chapitre 3 en fera un geste systématique : écrire la précondition avec la fonction, et l'exprimer par une assertion.

Prolongement : le calcul fautif ne servait même plus à rien après le décollage. Le système avait été conservé « au cas où » — un composant inutile a détruit une fusée.