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

                           MARDI 8 novembre, 10h30

                                -------------
                                Thibaut Girka
                                -------------

                           Université Paris Diderot

                 ============================================
                 Explaining Program Differences Using Oracles
                 ============================================

Program differences are pervasive in software development, but most of the
time they are represented as textual differences with no regards to the
syntactic nature of programming languages or their semantics. Thus, they may
be hard to read and often fail to convey insight on the changes on
semantics. Furthermore, such low-level, unstructured presentations are hard to
reason about.

We present a formal framework to characterize differences between
deterministic programs in terms of their small-step semantics. This
language-agnostic framework defines the notion of /difference languages/ in
which /oracles/—programs that relate small-step executions of pairs of program
written in a same language—can be written, reasoned about and composed.

We illustrate this framework by instantiating it on a toy imperative language
and by presenting several /difference languages/ ranging from trivial
equivalence-preserving syntactic transformations to characterized semantic
differences. Through those examples, we will present the basis of our
framework, show how to use it to relate syntactic changes with their effect on
semantics, how one can abstract away from the small-step semantics
presentation, and discuss the composability of oracles.

We will also discuss how our approach relates to "Refinement Mappings"
introduced by Abadi and Lamport and to "Differential Symbolic Execution"
coined by Person.