A Formally Verified Interpreter for the Shell-like Language CoLiS
The shell-like language CoLiS is described with abstract syntax trees and a formal semantics defined by inductive predicates. An interpreter is written in Why3 and proved correct and complete with respect to the semantics.
Authors: Nicolas Jeannerod
Topics: Inductive predicates / Ghost code
Tools: Why3
References: CoLiS project
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
why3doc index
- base : Formalization of CoLiS language
- interpreter : Interpreter
- lemmas : Lemmas on the CoLiS language
- mystrings
- skeleton
Generated by why3doc 0.87+git