Re: Typage

Il y a également une autre approche complémentaire à la question "es-ce que mon code fait ce pour quoi je l'ai codé et quoi qu'il arrive ?"

l'analyse statique permet de vérifier (ou pointer les défauts) d'un certain nombre de propriétés sur le code :
absence de division par zéro (ou bien alors pointer pourquoi elle pourrait arriver),
absence d'erreurs de pointeurs,
vérifier les valeurs des variables critiques (typiquement, est-ce que la puissance demandée au moteur peut devenir négative... ce qui est mauvais dans un avion ;-)
maîtrise de l'erreur dans le calcul flottant

(cf par exemple http://www.astree.ens.fr/)


Il convient également d'ajouter à cet outil des méthodes plus formelles, du type de celles exigées par les plus hautes qualifications EAL (critères communs), où des outils tels coq http://coq.inria.fr/coq-fra.html permettent de prouver mathématiquement que le code fait bien ce qu'il doit faire (modulo rayon cosmique permutant les bits tout de même ;-) ).
Le principe est d'écrire formellement les spécifications du programme, puis de les vérifier à l'aide de l'outil.