Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Théorème de Rice
Résumé
En informatique théorique, plus précisément en théorie de la calculabilité, le théorème de Rice énonce que toute propriété sémantique non triviale d'un programme est indécidable. Le théorème de Rice généralise l'indécidabilité du problème de l'arrêt. Le théorème est classique et fait l'objet d'exercices dans certains ouvrages de théorie de la calculabilité. Il a une certaine portée philosophique vis-à-vis de la calculabilité et est dû au logicien Henry Gordon Rice.
vignette|L'animation montre une machine impossible : d'après le théorème de Rice, il n'existe pas de machine qui lit des codes sources de fonctions et qui prédit si la fonction ne retourne jamais un entier non nul.
Les propriétés sémantiques concernent le comportement d'un programme et s'opposent aux propriétés syntaxiques sur le code source du programme. Une propriété est non triviale si elle n'est ni vraie pour toute fonction calculable, ni fausse pour toute fonction calculable. La table suivante donne des exemples de propriétés non triviales syntaxiques et des propriétés non triviales sémantiques. Le théorème de Rice ne s'applique qu'aux propriétés sémantiques.
Pour vérifier qu'un programme est correct, on peut recourir au test, y compris à des batteries de tests avec couverture de code. Mais comme l'a souligné Edsger Dijkstra .
La formulation pragmatique du théorème de Rice est qu'aucune méthode automatique d'analyse statique de programmes ne permet de décider, à partir du code source d'un programme, si la fonction qui associe les entrées à la sortie de ce programme satisfait ou non une propriété intéressante (non triviale) donnée.
En pratique, on adopte des stratégies pour contourner les limitations du théorème de Rice :
Vérification de programmes avec seulement un nombre fini d'états.
Méthode de vérification partiellement automatisée.
Méthodes à base d'approximations.
Méthodes restreignant l'ensemble des programmes sur lesquels on veut démontrer la propriété.
Restrictions raisonnables de l'ensemble des fonctions calculables.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.