Tu peux utiliser un outil comme Coq, qui peut vérifier à 100% qu'un code donné en Coq correspond bien à une spécification de haut-niveau (évidemment si celle-ci est incorrecte...), la solution existe donc, mais le coût d'utilisation d'une telle méthode pour écrire des programmes non-triviaux est énorme et complètement disproportionné par rapport aux bénéfices pour une entreprise normale. Maintenant il y a des cas où tu préfères que ton code soit certifié conforme à la spécification (le domaine médical, les logiciels d'avions de ligne, ... tous les cas mettant en jeu la vie humaine), mais même dans ces cas, les outils de certifications ne sont pas toujours utilisés. (J'ai parlé de Coq, mais ce n'est qu'un exemple, d'ailleurs mal adapté à un certain nombre d'autres contraintes souvent rencontrées dans les cas critiques (temps réel), il existe par exemple des méthodes de certification pour du C (ex : Caduceus), ...)
--
Jedaï
Partager