Towards Enabling Overture as a Platform for Formal Notation IDEs

TL;DR

This paper introduces the Overture platform, designed to enable reuse and extensibility for developing IDEs for formal methods, aiming to improve user experience and reduce development effort.

Contribution

It presents the design and extensibility principles of the Overture platform, facilitating reuse in creating formal notation IDEs and demonstrating its application through extensions.

Findings

Overture supports multiple language extensions.

The platform enables feature reuse across IDEs.

Extensions improve user experience for formal methods.

Abstract

Formal Methods tools will never have as many users as tools for popular programming languages and so the effort spent on constructing Integrated Development Environments (IDEs) will be orders of magnitudes lower than that of programming languages such as Java. This means newcomers to formal methods do not get the same user experience as with their favourite programming IDE. In order to improve this situation it is essential that efforts are combined so it is possible to reuse common features and thus not start from scratch every time. This paper presents the Overture platform where such a reuse philosophy is present. We give an overview of the platform itself as well as the extensibility principles that enable much of the reuse. The paper also contains several examples platform extensions, both in the form of new features and a new IDE supporting a new language.