Skip to Main content Skip to Navigation
Reports

Le langage CoLiS : syntaxe, sémantique et outillage

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.
Complete list of metadatas

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01614488
Contributor : Claude Marché <>
Submitted on : Wednesday, October 11, 2017 - 7:01:44 AM
Last modification on : Tuesday, April 21, 2020 - 1:06:31 AM
Document(s) archivé(s) le : Friday, January 12, 2018 - 12:54:22 PM

File

RT-0491.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

282

Files downloads

128