The CoLiS language: syntax, semantics and associated tools
Le langage CoLiS : syntaxe, sémantique et outillage
Résumé
This report presents the design choices of the CoLiS language, conceived within the ANR
project of the same name. We present the syntax of the language, both in an abstract and in a concrete
form, then we give typing rules, and finally its operational semantics. We describe a tool that implements
various operations applicable on CoLiS programs, mainly an interpreter and a translator to the shell language.
Operational semantics is defined formally within Why3, with which a formal proof of correction
of the interpreter is performed. Finally, we present some tooling for the execution of test campaigns for
non-regression and the detection of inconsistencies between direct interpretation and translation to the
shell.
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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...