Intervention de Gilles Dowek

Je reviens sur une autre question que vous avez posée tout à l'heure, relative à la probabilité qu'un bug se produise.

Prenons l'exemple du bug du Pentium, évoqué par Gérard Berry. Nous sommes face à un circuit qui fait des multiplications. Si on essaie de multiplier 3 par 4, cela fait 12 ; en revanche, si on multiplie 0 par 0 – et c'est là qu'il y a un bug – cela fait 256. S'interroger sur la probabilité que ce bug se produise revient à s'interroger sur celle que l'utilisateur de la calculette décide de faire cette multiplication de 0 par 0.

Cela nous amène à la première méthode, que personne n'a mentionnée, consistant, pour vérifier que des programmes sont corrects, à les tester, et donc à les utiliser. On fait une, puis trois, puis dix multiplications. Si le résultat est exact pour dix opérations, on se dit que le programme ou le circuit semble correct, et l'on s'arrête là. Cela définit les niveaux EAL les plus bas, soit 1 ou 2.

Il y a ensuite, au milieu de la gamme, d'autres critères. On demande au développeur d'exprimer formellement, sans établir de preuve, mais de manière très précise et mathématique, la spécification du programme.

Ce n'est qu'aux niveaux 6 et 7, les plus élevés, que l'on demande au développeur, non seulement d'exprimer ainsi ce que doit faire le programme, mais aussi de démontrer qu'il fait bien ce que l'on attend de lui.

Ces critères correspondent à des niveaux d'exigence et de coût variables. Pour certaines applications, le bug n'est pas très grave : c'est le cas par exemple pour un DVD, au contraire d'un avion de ligne. Mais parfois il se mesure en milliards de dollars. Or pour anticiper un bug d'un milliard de dollars, on peut s'offrir beaucoup de méthodes formelles …