Program testing and verification - WMM9MO73

Objectif(s)

Comprendre diverses approches pour tester et démontrer la correction de programmes, leurs forces et limitations.

Contenu(s)

Le plus souvent, pour se rendre compte de si un programme fonctionne correctement, on le teste, c'est-à-dire qu'on le lance, entièrement ou par parties, sur des exemples (parfois générés automatiquement) et on vérifie que les sorties vérifient la spécification. Même sans spécification, il est implicite que le programme ne doit pas « planter ».

Le test souffre d'une faiblesse majeure : il vérifie un nombre fini de cas, et un bug peut ne pas être détecté s'il ne se produit sur aucun de ces cas. Avec le test symbolique par exécution symbolique, le programme est exécuté avec certaines des valeurs d'entrées gardées symboliques : par exemple, au lieu de considérer qu'une variable _x_ vaut 5, on va la garder symbolique et explorer les comportements du programme pour toute valeur de _x_. Ceci est bien plus complet qu'en test normal (dit aussi test concret), mais aussi bien plus difficile : on doit en général explorer plusieurs chemins au sein du programme, ce qui impose l'usage d'algorithmes sophistiqués pour détecter les chemins impossibles. Comme tout garder symbolique est compliqué et coûteux, et parfois impossible (par exemple lors d'appels système), la plupart des outils mettent en œuvre un mélange d'exécution concrète et symbolique connu sous le nom de test concolique.

En général, le test symbolique ne peut prouver qu'un programme n'atteindra pas un bug, en raison du nombre possiblement infini de pas d'exécution à simuler. Prouver qu'un programme fonctionne comme on l'entendait est en fait comme prouver des théorèmes mathématiques : on prouve une propriété par récurrence sur le nombre de pas de calcul du programme (ou le nombre d'itérations de boucle, etc.). La grande difficulté de cela est que la propriété à démontrer par récurrence (dite invariant inductif) n'est pas nécessairement la propriété que l'on veut démontrer au final. Produire ces invariants inductifs est une activité difficile et fastidieuse pour les humains, et on a donc cherché à automatiser la production et la vérification du caractère inductif des invariants.

Des résultats de Turing (et Gödel etc.) montrent que l'automatisation générale des preuves de programmes et de théorèmes est impossible. Ceci n'exclut pas des solutions partielles et applicables industriellement.

Aisance en programmation.
Langage C.
Connaissances en logique du premier ordre et en mathématiques de base.