On peut considérer qu'un programme « fonctionne » lorsqu'il répond aux exigences fixées par les développeurs. Toutefois ces exigences peuvent être plus ou moins strictes : s'agit-il seulement d'avoir un programme qui ne crashe pas ou d'assurer que pour toute donnée bien formée qui lui est transmise, le programme retourne bien le résultat attendu ? C'est la notion de preuve informatique que nous touchons du doigt : contrairement aux tests qui ne portent nécessairement que sur des points précis, la preuve est complète, elle tient compte de tous les cas possibles. Nous n'allons pas rentrer dans le domaine théorique de la preuve informatique, domaine fort intéressant, mais qu'il serait vain de tenter de couvrir en quelques pages. Dans cet article, nous nous contenterons d'aborder un aspect pratique des preuves avec le framework Frama-C (FRAmework for Modular Analysis of C code).
1. Présentation et installation
- Accédez à tous les contenus de Connect en illimité
- Découvrez des listes de lecture et des contenus Premium
- Consultez les nouveaux articles en avant-première