Ne vous êtes vous jamais retrouvé devant un assert() qui saute et devoir lire des centaines de lignes de code avant de comprendre quel cheminement votre programme avait dû suivre pour en arriver là ? Ne vous êtes vous jamais posé la question de savoir si tout ce travail était réellement nécessaire ou s'il ne pourrait pas être délégué à un quelconque processus qui tourne en tâche de fond ? Ne se pourrait-il pas que les debuggers puissent évoluer et devenir capables de trouver ces bugs eux-mêmes sans intervention humaine ? Science-fiction ou réalité ?Cet article essaye de faire le point sur certaines techniques récentes de vérification logicielle et d'analyse de code et des répercussions possibles que ces récentes avancées pourraient avoir sur nos outils de debuggage dans un avenir proche.
1. Vérification formelle : mythes et réalités
Lorsqu'on parle de vérification formelle, on désigne en fait toutes les méthodes mathématiques qui tentent de produire des « logiciels corrects », c'est-à-dire exempt de bugs, via une exécution symbolique du programme. Tout naturellement, on en vient à se demander ce qu'est précisément un bug. En fait, on les définit couramment comme étant « l'ensemble des comportements non désirés du programme ».
Est-ce que tout est dit ? Absolument pas, car il faut pouvoir définir précisément, mathématiquement même, quel est le comportement correct du logiciel et cela nous mène immanquablement à la notion de « spécifications » qui définit les comportements corrects (ou incorrects) du logiciel.
La vérification formelle s'occupe donc de prouver mathématiquement la conformance d'un logiciel à un ensemble de spécifications jugées cruciales par les concepteurs. Cela ne veut pas dire qu'un logiciel correct est...
- 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
