A Meta-Approach to Describe Effectful and Distributed Semantics
Une méta-approche pour décrire des sémantiques distribuées et avec effets
Résumé
The study and production of programming language semantics is a computer science field aiming to represent these objects' behavior formally. The State-of-the-art presents different styles and technologies for working on semantics. Technologies have progressed a lot during the last four decades by proposing more and more frameworks adapted to carry out these studies. On the one hand, semantic styles have well-known positive characteristics and limitations. On the other hand, semantic tools are an active research topic. The thesis proposes a methodology for encoding semantics in a tiny functional meta-language called Skel. This language has a suite of tools for generating different artefacts for performing different types of studies. The methodology proposed in this thesis shows how to write concise semantics visually close to a programming language specification. To do so, we combined different algebraic constructs for writing precise, concise, readable, and easily maintainable formalizations. We have applied this technique to two case studies, the modeling of the JavaScript specification, ECMAScript, and the representation of a formal model to describe orchestration semantics representing the behavior of Internet of Things applications. These works give a clear idea of the potential and expressiveness of our formal framework, Skeletal Semantics. This manuscript is an introduction to Skeletal Semantics, showing how to produce usable and human-readable formalizations of different types of specifications - inference-rule based and in prose. In essence, the aim is to turn a mathematical representation of a language addressed to a specific category of researchers into valuable support for programmers to build real implementations.
L’étude de la sémantique des langages de programmation est un domaine de l’informatique visant à représenter formellement le comportement de programmes. L’état de l’art a beaucoup progressé au cours des quatre dernières décennies en proposant de plus en plus de cadres adaptés à la réalisation de ces études. S’il existe de nombreux styles, dont on connaît les caractéristiques positives et les limites, il reste encore beaucoup à faire en termes d’outils adaptés à la description et à l’étude de la sémantique des langages de programmation. Cette thèse s’inscrit dans ce contexte, en proposant une méthodologie pour pouvoir produire un objet représentant le comportement d’un langage de programmation, en fournissant tout ce qui est nécessaire pour pouvoir les étudier. La contribution de la thèse consiste à fournir une méthodologie pour écrire une sémantique concise et visuellement proche d’une spécification. Pour ce faire, nous utilisons un certain nombre de constructions algébriques qui, associées à notre approche purement fonctionnelle, conduisent à une formalisation claire, concise et facile à maintenir. Nous avons appliqué cette technique à deux études de cas, la modélisation de la spécification JavaScript, ECMAScript, et la représentation d’un modèle formel pour décrire la sémantique d’orchestration représentant le comportement des applications de l’internet des Objets. Ces travaux donnent une idée claire du potentiel et de l’expressivité de notre cadre formel, appelé sémantique squelettique. Ce manuscrit est à la fois une introduction à l’utilisation de la sémantique squelettique et son application aux langages de programmation, même quand ceux-ci ont une spécification complexe et de taille conséquente. C’est également une étude de la manière d’exploiter les caractéristiques d’un tel outil pour produire des formalisations qui peuvent être claires et lisibles par l’homme. En substance, il s’agit de faire d’une représentation mathématique d’un langage, qui s’adresse à une catégorie spécifique de chercheurs, un support précieux pour les programmeurs en vue d’implémentations réelles.
Origine : Version validée par le jury (STAR)
