Interprétation abstraite
De Wikipedia, l'encyclopédie 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 le professeur Patrick Cousot et le docteur Radhia Cousot.