Interprétation abstraite
From Wikipedia, the free encyclopedia
L'interprétation abstraite est une théorie d'approximation de la sémantique de programmes informatiques fondée sur les fonctions monotones pour ensembles ordonnés, en particulier les treillis (en anglais : lattice). Elle peut être définie comme une exécution partielle d'un programme pour obtenir des informations sur sa sémantique (par exemple, sa structure de contrôle, son flot de données) sans avoir à en faire le traitement complet.
Sa principale fonction concrète est l'analyse statique, l'extraction automatique d'informations sur les exécutions possibles d'un programme ; ces analyses ont deux usages principaux :
- pour les compilateurs, afin d'analyser le programme pour déterminer si certaines optimisations ou transformations sont possibles ;
- pour le débogage, ou pour prouver l'absence de certains types de bugs dans le programme.
L'interprétation abstraite a été formalisée par les professeurs Patrick Cousot et Radhia Cousot.
Commençons par définir l'interprétation abstraite dans un exemple concret et non informatique.
Considérons les personnes présentes dans une salle de conférence. Si nous voulons prouver que certaines personnes n'étaient pas présentes, une des manières de faire serait de tenir une liste comprenant le nom et le numéro de sécurité sociale de tous les participants.
Nous aurions cependant aussi pu nous limiter à enregistrer seulement leurs noms. Si le nom d'une personne est introuvable dans la liste, nous pouvons en conclure que cette personne n'était pas présente ; mais s'il l'est, nous ne pouvons pas pour autant être absolument certain de sa présence, en raison des possibilités d'homonymes. Notons que cette information, bien qu'imprécise, est toutefois adéquate dans la plupart des cas - en effet, les homonymes sont plutôt rares en pratique.
Si nous ne sommes intéressés qu'à une information spécifique, comme « Y a-t-il une personne âgée de n ans dans la salle », il n'est pas nécessaire de garder une liste de tous les noms et toutes les dates de naissance. Nous pouvons, sans perdre de précision, nous restreindre à maintenir une simple liste de l'âge des participants. Et si cela était encore trop dur à gérer, nous pourrions encore ne garder que l'âge minimal m et l'âge maximal M. Si la question concerne un âge strictement inférieur à m ou strictement supérieur à M, nous pouvons affirmer que cette personne n'était pas présente. Dans les autres cas, nous sommes dans l'incapacité de répondre.
En informatique, il est en général impossible d'analyser exhaustivement un programme quelconque dans un temps fini (voir le théorème de Rice et le problème de l'indécidabilité de la terminaison d'un programme). Des abstractions sont utilisées pour simplifier ces problèmes vers des problèmes pour lesquels une solution peut-être décidée de manière automatique. Le problème crucial est de diminuer la précision afin de rendre les problèmes gérables tout en gardant suffisamment de précision pour répondre à la question (comme « Le programme peut-il planter ? ») qui nous intéresse.
