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
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 metadatas

Cited literature [5 references]  Display  Hide  Download

Contributor : Claude Marché <>
Submitted on : Wednesday, October 11, 2017 - 7:01:44 AM
Last modification on : Thursday, April 5, 2018 - 12:30:22 PM
Long-term archiving on : Friday, January 12, 2018 - 12:54:22 PM


Files produced by the author(s)


  • HAL Id : hal-01614488, version 1


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⟩



Record views


Files downloads