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

https://hal.inria.fr/hal-01614488
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

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

233

Files downloads

83