L'analyse statique ne peut pas prouver que votre avion ne s'écrasera pas. Elle peut prouver quelque chose de plus utile.
L'interprétation abstraite sur-approxime chaque état possible du programme. Si une division par zéro est inaccessible dans l'abstraction, elle est inaccessible dans le code réel. Voici comment cela fonctionne et où cela atteint ses limites.
L'analyse statique ne peut pas prouver qu'un avion ne s'écrasera pas. Elle peut prouver que la boucle de contrôle de votre altimètre ne divisera jamais par…