DEVELOPPEMENT D’UN SERVEUR DE LANGAGE POUR LE B

Objectif du stage :  CLEARSY conçoit et développe des systèmes critiques sûrs en s’appuyant sur la méthode formelle B et le B événementiel au moyen logiciel Atelier B. Les ingénieurs utilisent cet atelier pour écrire et prouver leurs modèles, mais les outils d’édition modernes (VS Code, Eclipse, éditeurs web) ne disposent pas d’une assistance aussi avancée pour les langages B et B événementiel : coloration syntaxique, absence de diagnostics en temps réel, pas de complétion ni de navigation.

La société a publié sous licence GPL-3.0 le projet BCOMPILER[1], qui fournit bcomp, un front-end C++ d’analyse syntaxique et de vérification de types des fichiers B, et bxml, qui produit des arbres syntaxiques abstraits décorés (BXML) représentant les composants B. Le projet fournit également des bibliothèques qui permettent d’accéder à diverses fonctionnalités utiles à la réalisation d’un serveur de langage (gestion des références croisées, par exemple).

L’objectif du stage est de concevoir et développer un serveur de langage conforme au protocole LSP (Language Server Protocol) pour les langages de la méthode B et le B événementiel, en s’appuyant notamment sur les fonctionnalités de BCOMPILER pour l’analyse syntaxique, la vérification de types et la production de l’AST décoré.

Le plan du stage est le suivant :

• Étudier le protocole LSP, les serveurs de langage existants et le code de BCOMPILER.
• Concevoir l’architecture du serveur : communication JSON-RPC, gestion de documents, intégration du front-end C++.
• Développer les fonctionnalités suivantes : diagnostics (syntaxe et typage), complétion, définition et références, surbrillance des symboles, mise en forme, renommage, arborescence de symboles et documentation au survol.
• Réaliser une extension cliente (VS Code ou équivalent) pour valider le serveur sur des projets B réels.
• Évaluer les performances (réactivité, projets de grande taille), documenter et publier le travail (code source open source et rapport de stage).

Profil et compétences recherchées :

Étudiant(e) en 3ᵉ année d’école d’ingénieurs. Maîtrise de C++ ou d’un langage typé (Rust, Java, OCaml…), intérêt pour la théorie des langages (analyse syntaxique, compilation), notions de méthodes formelles appréciées. Goût pour le travail en équipe et le développement open source.

[1]https://github.com/CLEARSY/BCOMPILER