FM 2021

Tutorial on “Implementing an IDE for “tiny” Event-B with JetBrains Metaprogramming System MPS” will be organized at the 23rd International Symposium on Formal Methods (FM 2021), to be held online.

Brief description

The goal of the tutorial is to give a brief overview of structural code editing and to demonstrate how an Integrated Development Environment (IDE) for a subset of the Event-B specification language can be implemented (modeling perspective only) using a state-of-the-art tool JetBrains MPS.

The tutorial starts with a discussion on language workbenches, which are tools designed to define, reuse and compose programming and domain-specific languages together with their IDEs. It continues with a discussion on projectional (structured) editing, an alternative to mainstream text-based editing that allows overcoming the limits of language parsers. The main part of the tutorial focuses on implementing a simplified version of the Event-B specification language using JetBrains MPS, which is a projectional language workbench that can be used to build code editors supporting textual, tabular and graphical notations.

The simplified version of the Event-B language will support defining contexts and machines, and the IDE implemented during the tutorial will support validation of the static semantics (e.g., that all referred identifiers have been declared before) and will provide standard editor features such as syntax-aware autocomplete menus, simple code refactorings (e.g., “negate a guard“, “reorder invariants“, “sort variables alphabetically“), error reporting, and so on. Special attention will be given to implementing the support of the mathematical notation in expressions.

It is important to note the limitation of the extent to which the Event-B language will be implemented: the aim is to showcase a wide range of functionality of JetBrains MPS, rather than to have a full-fledged implementation of the Event-B language constructs.

Target audience and requirements

The proposed tutorial will present JetBrains MPS from the ground, without any previous knowledge on language development required from the participants. The tutorial will be interactive and after the tutorial the participants will have implemented an MPS-based IDE for a “tiny” version of Event-B. The tutorial is intended for those interested in implementing tooling for specification languages, and requires basic programming skills in Java or another object-oriented programming language.

More information coming soon.