Interprétation abstraite
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 le professeur Patrick Cousot et le docteur Radhia Cousot.
Définition[modifier | modifier le code]
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.
Interprétation abstraite de programmes informatiques[modifier | modifier le code]
Étant donné un langage de programmation ou de spécification, l'interprétation abstraite consiste à déterminer des sémantiques liées par des relations d'abstraction. La sémantique la plus précise, décrivant l'exécution réelle du programme de manière très fidèle, est appelée sémantique concrète. Par exemple, la sémantique concrète d'un langage de programmation impératif peut associer à chaque programme l'ensemble des traces qu'il produit - une trace d'exécution étant une séquence des états consécutifs possibles de l'exécution d'un programme ; un état étant constitué de la valeur du compteur de programme et des emplacements mémoire utilisés (globale, pile et tas). Des sémantiques plus abstraites en sont alors déduites ; par exemple, on pourra ne considérer que l'ensemble des états atteignables lors des exécutions (ce qui revient à ne considérer que les derniers états des traces).
Pour permettre l'analyse statique, certaines sémantiques calculables doivent être déduites. Par exemple, on pourra choisir de représenter l'état d'un programme manipulant des variables entières en oubliant les valeurs proprement dites et en ne gardant que leurs signes (+, - ou 0). Pour certaines opérations élémentaires comme la multiplication, une telle abstraction ne perd pas de précision : pour connaître le signe d'un produit, il est suffisant de connaître le signe des opérandes. Pour d'autres opérations en revanche, l'abstraction perdra de la précision : ainsi, il est impossible de connaître le signe d'une somme dont les opérandes sont de signe contraire.
De telles pertes de précision ne peuvent pas, en général, être évitées lorsque l'on fait des sémantiques décidables. Il y a, en général, toujours un compromis à faire entre la précision de l'analyse et sa faisabilité, que ce soit vis-à-vis de la calculabilité ou de la complexité.
Formalisation[modifier | modifier le code]
