Skip to Main content Skip to Navigation
Reports

Le langage CoLiS : syntaxe, sémantique et outillage

Abstract : 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.
Complete list of metadata

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 : Thursday, July 8, 2021 - 3:49:47 AM
Long-term archiving on: : 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

326

Files downloads

163