Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                          Lundi 18 septembre, 11h30

                              -----------------
                              Nicolas Jeannerod
                              -----------------

                           Université Paris Diderot

             ====================================================
             Formalising an intermediate language for POSIX shell
             ====================================================

The POSIX shell language has semantics that present unique traits: the
control flow can be very surprising, the expansion mechanism has a
huge expressive power hidden behind apparently insignificant details,
the scoping is entirely dynamic…

These pitfalls make it really hard to write safe scripts or
trustworthy analysers. A first step towards writing such tools is thus
to formalise semantics for shell or a reasonable subset.

In this talk, I will introduce an intermediate language, “CoLiS”,
that, on the one hand, is close enough to shell to be the target of an
automated translation of the scripts that interest us, and, on the
other hand, has well-defined static semantics.

Its syntax and semantics are formalised in the proof environment Why3,
as well as an interpreter, that is proven both sound and complete with
respect to the formal semantics.