Hina

Notes d'informatique théorique.

Page principale A propos du blog Me contacter

Interprétation Abstraite : idée informelle

L'interprétation abstraite est une théorie qui s'intéresse notamment à l'analyse de programmes informatiques au moyen d'approximations de leur comportement. Certes. Pourquoi est-ce qu'on se ferait chier avec ça ?

Première partie de la question

D'abord, pourquoi aurions-nous besoin d'analyser des programmes informatiques ?

Parmi les nombreux systèmes (partiellement) informatisés, il en existe une certaine classe pour lesquels il est important de donner des garanties de sureté. Ce sont les systèmes critiques, que l'on croise dans les contextes qui mettent des vies en jeu : l'aviation, l'éarospatiale, les systèmes de défense militaires, les projets liés aux énergies, comme les centrales nucléaires, les systèmes pour le médical...

Le but est alors de trouver un moyen de savoir décrire avec précision le comportement de tels systèmes et de garantir à un certain niveau qu'ils répondent à des critères de sureté qu'on leur impose.

Seconde partie de la question

Mais pourquoi aurions-nous besoin d'approximer le comportement de tels systèmes ?

La réponse originelle se trouve dans l'énoncé du théorème de Rice. On peut en trouver de plusieurs versions, qui correspondent à différents usages.

Une première version qui parle essentiellement de machines de Turing, que l'on trouve couramment dans un cours de calculabilité ou sur wikipédia :

Pour toute propriété non triviale $P$ sur les langages récursivement énumérables, le problème de savoir si le langage $\mathcal{L}(\mathcal{M})$ d'une machine de Turing $\mathcal{M}$ vérifie $P$ ou non est indécidable.

Une autre version, orientée génie logiciel, provenant du cours de sémantique de l'ENS qui attire particulièrement notre attention :

Considering a Turing complete language, any non trivial semantic specification is not computable.

Désobfusquons ces énoncés :

Énoncé 1 : La non-trivialité d'une propriété désigne le fait qu'elle ne soit pas, soit vraie pour tous les langages récursivement énumérables, soit fausse pour tous les langages récursivement énumérable.
Ainsi, il n'existe aucune machine de Turing qui, étant donné une propriété non triviale sur les langages récursivement énumérables, nous dise si un langage récursivement énumérable quelconque vérifie cette propriété.
Énoncé 2 : Pour cet énoncé, il n'est pas nécessaire de tenter de se battre avec les termes utilisés. Mais définissons les plus subtils d'entre eux.
Un langage Turing complete est un langage dont tous les programmes peuvent être encodés dans une machine de Turing. On peut leur faire calculer tout ce qui est calculable.
Une spécification sémantique est un ensemble correct d'exécutions d'un programme.
Ainsi, l'énoncé signifie moralement qu'il n'existe pas d'algorithme qui, à partir d'un code, décide des spécifications non triviales.

Ce théorème est une véritable barrière aux barreaux d'aciers pour les tentatives d'analyse de programmes informatiques, puisqu'il établit l'impossibilité de trouver une méthode qui montre qu'un programme vérifie une propriété P non triviale, et qui soit à la fois :

correcte (sound) : si l'analyse dit "tel programme vérifie P", alors elle ne se trompe pas
complète : si un programme A vérifie P alors l'analyse le dira si on lui demande d'analyser A
automatique : l'analyse ne nécessite pas l'intervention d'un humain

Mais comme toute barrière, elle n'est pas complètement opaque. Nous distinguons certaines allures au travers de ses barreaux.

Ne pourrions nous pas tenter de déployer notre force de réflexion, sans pour autant passer la barrière ?

Nos chercheurs et nos ingénieurs ont construit et exploré de nombreuses méthodes d'analyse partielle qui ont chacunes leurs avantages et leurs faiblesses. Les trois grandes méthodes de vérification formelle qui sont encore de nos jours étudiées par les chercheurs sont les suivantes :

Model checking : ici, on se ramène autant que possible à des programmes qui terminent, pour pouvoir explorer un ensemble fini d'exécutions et en dire des choses intéressantes.
Assistants de preuve : ici, on crée des algorithmes qui analysent des programmes avec l'aide des humains pour en dire des choses intéressantes.
Analyse statique sur des abstractions : ici, on abstrait le comportement de nos programmes pour créer des algorithmes autonomes qui disent des choses intéressantes. On s'intéresse à cette méthode dans ce post.