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. 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.