Théorème de Rice

Le théorème de Rice généralise et amplifie considérablement le résultat du problème de l’arrêt. Il affirme, en substance, que toute question intéressante portant sur ce qu’un programme fait vraiment, c’est-à-dire sur son comportement et non sur la façon dont il est écrit, est indécidable. Autrement dit, il n’existe aucune méthode mécanique capable de déterminer à coup sûr, pour n’importe quel programme, s’il possède telle ou telle propriété relative à son résultat: savoir si un programme calcule toujours un nombre positif, s’il donne jamais tel résultat particulier, s’il traite correctement toutes ses données, ou s’il ne fait rien du tout. Seules échappent à ce verdict les propriétés triviales, celles qui sont vraies pour tous les programmes ou fausses pour tous, et qui ne présentent donc aucun intérêt pratique.

Ce théorème a été démontré par Henry Gordon Rice en 1951, dans le prolongement direct des travaux de Turing des années 1930. Il faut bien saisir la distinction sur laquelle il repose: on peut parfaitement examiner le texte d’un programme, compter ses lignes ou vérifier s’il contient un certain mot, car ce sont des propriétés du code lui-même. Ce que le théorème interdit d’automatiser, c’est la prédiction certaine de ce que ce code produira une fois exécuté. La forme d’un programme est accessible à l’analyse, mais sa signification, le comportement qu’il déploie effectivement, échappe à toute décision mécanique générale.

Ce résultat a une portée pratique considérable pour qui conçoit des logiciels d’analyse. Il explique pourquoi aucun antivirus ne peut identifier avec une certitude absolue tout programme malveillant à partir de son comportement, pourquoi aucun outil ne peut prouver automatiquement qu’un code fait exactement ce qu’on attend de lui, et pourquoi la vérification parfaite des programmes restera toujours hors d’atteinte dans le cas général. Les informaticiens s’en accommodent en développant des méthodes approchées, des analyses qui se trompent parfois dans un sens prudent, ou des vérifications limitées à des programmes suffisamment simples pour qu’une réponse fiable redevienne possible.