Le langage CoLiS : syntaxe, sémantique et outillage

Ilham Dami 1 Claude Marché 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Ce document présente les choix de conception du langage CoLiS, conçu dans le cadre du projet ANR du même nom. On présente la syntaxe du langage, à la fois sous une forme abstraite et une forme concrète, puis des conditions de bon typage et enfin sa sémantique opérationnelle. On décrit ensuite un outil qui implémente différentes opérations applicables sur les programmes CoLiS, principalement un interpréteur et un traducteur vers le langage shell. La sémantique opérationnelle est définie formellement au sein de l’environnement Why3, avec lequel une preuve formelle de correction de l’interpréteur est réalisée. Enfin, on présente un outillage visant à l’exécution de campagnes de test de non-régression et de détection d’incohérences entre l’interprétation directe et la traduction vers le shell.
Type de document :
Rapport
[Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22
Liste complète des métadonnées

Littérature citée [5 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01614488
Contributeur : Claude Marché <>
Soumis le : mercredi 11 octobre 2017 - 07:01:44
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : vendredi 12 janvier 2018 - 12:54:22

Fichier

RT-0491.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01614488, version 1

Citation

Ilham Dami, Claude Marché. Le langage CoLiS : syntaxe, sémantique et outillage. [Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22. 〈hal-01614488〉

Partager

Métriques

Consultations de la notice

182

Téléchargements de fichiers

47