Sous-projet 7 : Langage de propriétés

Description du sous-projet, responsable, partenaires

Élaboration d'un langage de propriétés pour les programmes C

Début : M1

Fin : M12

Responsable : INRIA

Participants : INRIA, CEA, AF

Objectifs du sous-projet

Un langage de spécification pour les programmes C a été conçu par l'équipe PROVAL pour l'outil Caduceus en s'inspirant de JML (Java Modeling Language), un langage de spécification similaire pour les programmes Java. Ce langage conserve de JML les aspects suivants : logique du premier ordre, spécification à la Hoare (pré-conditions, post-conditions, assertions, invariants), et partage des expressions sans effets de bord avec le langage C. Ce langage comporte tout de même un certain nombre de différences avec JML, les principales étant l'arithmétique de pointeurs propre au langage C d'une part, et la possibilité de déclarer des symboles de fonctions et des prédicats d'autre part. De plus contrairement à JML, notre langage devra permettre de décrire l'environnement d'exécution et de compilation des programmes : en effet un programme Java est exécuté sur une machine virtuelle normalisée alors que les programmes C sont exécutés sur des systèmes de natures très hétérogènes.

Si ce langage de spécification est déjà satisfaisant sur un grand nombre de points, il reste nécessaire de l'étendre afin de pouvoir d'une part spécifier des propriétés qui ne peuvent pas l'être pour l'instant (telles que des propriétés inductives sur les structures chaînées), et d'autre part spécifier plus facilement d'autres propriétés (accès à des ensembles de bits consécutifs, par exemple).

Détails des réalisations et échéances

T7.0 Intégration du langage de spécification de Caduceus dans l'infrastructure générique (SP2)

Cette tâche consiste à intégrer le langage de spécification existant, développé pour l'outil Caduceus dans l'équipe PROVAL, dans l'infrastructure générique. La fonctionnalité correspondante est la possibilité de réaliser les analyses syntaxique et sémantique (typage) d'une annotation à un point donné du programme.

T7.1 Extension du langage

Le langage de spécification développé dans le cadre de Caduceus comporte encore des limitations. Certaines sont uniquement pratiques, c'est-à-dire correspondent à des propriétés qu'il est théoriquement possible d'écrire dans le langage de spécification mais pas de manière concise, comme par exemple la désignation d'un sous-ensemble de bits consécutifs d'une expression entière. D'autres limitations plus sévères correspondent à des propriétés qu'il est actuellement impossible d'écrire dans le langage de spécification (sans recourir à l'aide de prédicats externes définis seulement du côté de l'outil de preuve), telle que la propriété pour une structure de données de former une liste chaînée. Cette tâche a pour but de remédier à ses limitations.

T7.2 Documentation (tutoriel, manuel de référence, exemples)

Le langage de spécification sera documenté sous la forme d'un manuel de référence donnant sa syntaxe et sa sémantique, d'un tutoriel montrant son utilisation pas à pas sur un exemple concret, et d'un ensemble de programmes C annotés donnés à titre d'exemples. À cette occasion un site internet sera créé à des fins de dissémination du langage de spécification lui-même, les outils développés dans CAT n'étant considérés que comme un support pour cette dissémination.

T7.3 Évaluation sur des cas réels

Le langage de spécification sera évalué sur des cas réels, en annotant des programmes sources existants à l'aide du langage de spécification (sans chercher à faire de preuve, mais en réalisant les analyses syntaxique et de typage des programmes annotés).

Critère d'évaluation du résultat et de décision de poursuite du sous-projet

Le succès de ce sous-projet sera évalué par la tâche T7.3, c'est-à-dire en mesurant l'adéquation du langage pour spécifier des codes C typiques du monde de l'embarqué.

Un autre critère d'évaluation à moyen terme sera le taux de dissémination du langage dans la communauté. À long terme la création d'une norme pourra être envisagée.

Tâche

Resp.

Début

Fin

Charge (homme/mois)

Délivrables

CEA

INRIA

IRISA

DA

AF

SVDO

FT

T7.0

INRIA

M1

M3

2

2






Prototype

T7.1

INRIA

M3

M7

4

4






Prototype

T7.2

INRIA

M7

M9

2

2






Rapport

T7.3

INRIA

M9

M12

4

4






Rapport d'évaluation