Imprimer |
Necro, la sémantique sans y laisser les os : conception d’un système formel de description et de manipulation de sémantiques opérationnelles (Necro, the skeleton key to semantics) Noizet, Victoire - (2022-09-29) / Universite de Rennes 1 - Necro, la sémantique sans y laisser les os : conception d’un système formel de description et de manipulation de sémantiques opérationnelles
| |||
Langue : Français Directeur(s) de thèse: Schmitt, Alan Discipline : Informatique Laboratoire : IRISA Ecole Doctorale : MATHSTIC Classification : Informatique Mots-clés : spécification, sémantique opérationnelle, formalisation, interpréteur, débogueur
| |||
Résumé : Les langages de programmation ont rarement une sémantique définie de manière formelle. Pourtant, c'est la seule manière de garantir l'unicité de l'interprétation d'un langage. Une des raisons qui expliquent ce manque est la difficulté d'écrire une sémantique, et le peu d'application qu'on peut en faire. Nous proposons donc Skel, un langage simple qui permet d'écrire des sémantiques opérationnelles de langage, et Necro, un écosystème pour les manipuler, et notamment générer des interpréteurs ou des débogueurs à partir de celles-ci. De plus, Necro est extensible, et le langage Skel est minimal, de sorte qu'il est simple de rajouter un backend pour extraire la sémantique vers d'autres outils. Abstract : Programming languages rarely have a formally defined semantics, although it is the only way to ensure unicity in the interpretation of a language. On of the main reasons thereof is how hard it is to write a semantics, and how few applications there is. To this end, we introduce Skel, a simple language to describe programming languages' operational semantics, and Necro, an ecosystem to manipulate them, allowing among other things to generate interpreters and debuggers. Furthermore, Skel being minimal, and Necro being extensible, it is easy to add a new backend, in order to extract Skel semantics to other tools. |