Description
Date depot: 1 janvier 1900
Titre: Aide à la preuve automatique de programmes SPARK par génération d'annotations intermédiares
Encadrante :
Maria Virginia APONTE (CEDRIC)
Directrice de thèse:
Véronique VIGUIÉ DONZEAU-GOUGE (CEDRIC)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Dans cette thèse, il s’agira de concevoir des algorithmes de génération d’annotations internes pour le langage de programmation SPARK en s’appuyant sur une analyse préalable des besoins réels des utilisateurs de l’approche SPARK. On mettra donc à profit le corpus conséquent de programmes déjà écrits et prouvés dans ce langage afin de traiter un maximum de programme ≪réels≫.
Le langage de programmation SPARK est un sous-langage d’Ada. Etant dédié à l’écriture de programmes sûrs, il est fortement contraint: fonctions sans effets de bord, initialisation en bloc des tableaux, pas de pointeurs, pas de partage mémoire, etc. Parmi les annotations insérées par l’utilisateur dans le code source de son programme, on distingue deux sortes: les annotation externes et les annotations internes aux programmes. Les annotations externes aux programmes constituent la spécification de ceux-ci (contrats de sous-programmes, invariants de types). Elles correspondent à la spécification de comportement des programmes et sont donc écrites assez facilement par le programmeur. Par exemple, un sous-programme d’insertion triée d’un entier dans un tableau d’entiers pourra spécifier comme pré-condition que le tableau d’entrée est trié, et comme post-condition que le tableau après insertion contient le nouvel élément, et qu’il est toujours trié. Les annotations internes aux programmes (invariants de boucle, assertions en un point, contrats de sous-programmes locaux) correspondent à des étapes de preuve nécessaires pour garantir la validité des annotations externes. Les programmeurs ont généralement beaucoup plus de difficultés à les écrire: elles requièrent une grande expertise et leur mise en œuvre est un frein à l’adoption de SPARK par un plus grand nombre d’utilisateurs. L’ensemble d’outils SPARK permet l’automatisation d’une partie importante des tâches de vérification. Le reste de ces tâches, comprenant principalement l’ajout d’annotations supplémentaires nécessaires pour accomplir la preuve automatique des annotations externes, doit être réalisé manuellement par le programmeur. L’objectif de cette thèse est d’augmenter le degré d’automatisation apporté par l’approche SPARK, via la génération automatique d’annotations internes au code SPARK. Il en découlera une utilisation plus simple de SPARK et également une plus grande automatisation des preuves des annotations externes.
Le déroulement envisagé est le suivant: d’abord s’intéresser à des génération d’invariants simples en élaborant la justification théorique en parallèle, puis continuer avec des invariants et annotations plus complexes.
L’originalité et la richesse de ce sujet tiennent dans l’équilibre entre deux atouts: d’une part la relative simplicité des structures de programmation à analyser vu les contraintes de la programmation SPARK et d’autre part le ≪réealisme≫ des programmes visés vu l’utilisation de SPARK dans l’industrie des logiciels critiques et du corpus de programmes disponibles.
Doctorant.e: Sango Marc