Séminaire des équipes de recherche
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.
- Date : 8/11/2016
- Lieu : Inria Paris - 2 rue Simone Iff - Salle Lions 1, bâtiment C
- Intervenant(s) : Thibaut Girka (Université Paris Diderot)
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.