Interpretation abstraite

Interpretation abstraite

Interprétation abstraite

L'interprétation abstraite est une théorie d'approximation de la sémantique de programmes informatiques basé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 Pr Patrick Cousot et le Dr Radhia Cousot.

Sommaire

Définition

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 toujours 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 agé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 en gardant suffisamment pour répondre à la question (comme « le programme peut-il planter? ») qui nous intéresse.

Interprétation abstraite de programmes informatiques

É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 locations mémoires utilisées (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 êtres 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

À voir

Liens externes

Ce document provient de « Interpr%C3%A9tation abstraite ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Interpretation abstraite de Wikipédia en français (auteurs)

Игры ⚽ Нужно решить контрольную?

Regardez d'autres dictionnaires:

  • Interprétation Abstraite — L interprétation abstraite est une théorie d approximation de la sémantique de programmes informatiques basée sur les fonctions monotones pour ensembles ordonnés, en particulier les treillis (en anglais : lattice). Elle peut être définie… …   Wikipédia en Français

  • 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… …   Wikipédia en Français

  • Interpretation — Interprétation Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom …   Wikipédia en Français

  • Interprétation (homonymie) — Interprétation Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom …   Wikipédia en Français

  • Interprétation conservatrice — Interprétation Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom …   Wikipédia en Français

  • Interprétation — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Sur les autres projets Wikimedia : « Interprétation », sur le Wiktionnaire (dictionnaire universel) D une manière générale, le mot… …   Wikipédia en Français

  • Interpretation (informatique) — Interprète (informatique) Pour les articles homonymes, voir Interprète et Interpréteur. Un interprète, ou interpréteur (voir infra), est un outil informatique ayant pour tâche d analyser, de traduire et d exécuter un programme écrit dans un… …   Wikipédia en Français

  • Interprétation (informatique) — Interprète (informatique) Pour les articles homonymes, voir Interprète et Interpréteur. Un interprète, ou interpréteur (voir infra), est un outil informatique ayant pour tâche d analyser, de traduire et d exécuter un programme écrit dans un… …   Wikipédia en Français

  • L'interprétation par téléphone — Interprétation Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom …   Wikipédia en Français

  • Famille abstraite de langages — En informatique théorique, et en particulier en théorie des langages formels, le terme famille abstraite de langages réfère à une notion qui généralise des caractéristiques communes aux langage rationnels, aux langages algébriques, aux langages… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”