CE48 - Fondements du numérique : informatique, automatique, traitement du signal

Vers un langage de spécification et un écosystème pour spécifier, tester et vérifier des programmes OCaml – GOSPEL

Résumé de soumission

Le projet GOSPEL vise à enrichir la définition de Gospel, un langage de
spécification pour OCaml; à développer un écosystème d'outils basés sur
Gospel; et à effectuer un certain nombre d'études de cas permettant d'éprouver
expérimentalement l'utilisabilité de Gospel.

Gospel permet d'annoter du code OCaml avec une spécification qui décrit
comment ce code est utilisé et quel service il rend. Cette spécification est
ensuite utilisée par divers outils pour engendrer de la documentation,
effectuer des tests automatisés, et vérifier la correction fonctionnelle de ce
code.

Gospel vise à devenir un standard de fait, que les programmeurs peuvent
apprendre aisément, et que les outils peuvent adopter comme base commune.

Nous choisissons OCaml parce qu'il offre une combinaison unique de simplicité,
de pouvoir expressif, d'efficacité, et de stabilité à long terme, et parce
qu'il est utilisé dans le monde universitaire et dans l'industrie pour
développer des logiciels complexes et critiques. Comparé à des langages de
plus bas niveau, OCaml supprime plusieurs sources potentielles de comportement
aberrant, ce qui facilite la vérification de programmes, mais propose
également des moyens puissants pour assembler un programme à partir de
composants élémentaires, ce qui rend la spécification plus difficile.

Nous souhaitons démontrer que Gospel permet de détecter des erreurs auxquelles
le système de types d'OCaml est insensible, d'où une sûreté accrue pour un
surcoût limité.

Nos principaux objectifs sont de:

1. Développer le langage Gospel, de façon à accroître son pouvoir expressif,
tout en préservant sa simplicité.

2. Développer l'écosystème des outils fondés sur Gospel, dont le typeur de
Gospel, l'IDE Merlin, et des outils de documentation, de test, et de
vérification.

3. Éprouver Gospel et en démontrer l'intérêt via des études de cas, allant de
bibliothèques simples jusqu'à des composants logiciels complexes tirés
d'applications industrielles critiques.

Coordinateur du projet

Monsieur François Pottier (Institut national de la recherche en informatique et automatique)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Tarides
Institut national de la recherche en informatique et automatique
LMF UPSaclay - Laboratoire Méthodes Formelles
Nomadic Labs

Aide de l'ANR 481 103 euros
Début et durée du projet scientifique : décembre 2022 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter