Sites Inria

English version

Séminaire des équipes de recherche

Interactive execution of a formal semantics

© INRIA Sophie Auvin - G comme Grille

  • Date : 4/07/2016
  • Lieu : 2 rue Simone Iff, 75012 Paris - Salle Jacques-Louis Lions 1, bâtiment C - 10h30
  • Intervenant(s) : Arthur Charguéraud

In previous work, we built a formal semantics for JavaScript. This semantics is faithful to the standard (EcmaScript, version 5), and can be executed on test programs. In this talk, I will describe ongoing efforts for making such a formal semantics more likely to be eventually adopted as the reference semantics by the JavaScript committee.

I will present the details of the functional semantics that we set up, and describe a tool for executing this semantics. Our tool is an interactive debugger that supports step-by-step execution of the specification on concrete programs. Compared with a traditional debugger, our debugger is specialized for interpreters: it allows to visualize not only the complete state of the interpreter program but also the complete state of the interpreted program.

Moreover, it supports arbitrary breakpoint conditions constraining the interpreter program and/or the interpreted program.

Mots-clés : Interactive Execution Semantics Séminaire Gallium Formal

Haut de page

Suivez Inria