A Semantics-Aware Text Editor for Event-B
Author
Abstract
Text editors are common editing tools for many modeling and programming languages. Due to their wide-spread acceptance and the multifaceted application of text editing in general, users are accustomed with this way of editing. The Rodin platform for the Event-B method has been developed during the Rodin EU Framework 6 project and is now being deployed in industry in the EU Framework 7 project Deploy. Rodin models are stored in a database and thus far only a structural, graphical editor has been provided to input and modify the models. This has turned out to be very cumbersome for larger models, and industrial partners have repeatedly requested a textual representation along with a proper text editor.
With this work we introduce a comprehensive, state-of-the-art text editor for the Event-B method. It is well integrated with the Rodin platform and the existing graphical editor. It is based on the Eclipse text editor framework and provides a user interface which complies with modern usability standards. The text editor offers common features such as:
- Copy-paste and moving of text blocks
- Syntactic and semantic highlighting
- Code completion
- Outline view and quick navigation
- Error marking
- Printing support
For the text editor we have designed a text syntax for Event-B models. It allows to represent all core Event-B elements. The syntax is an adaption of the existing graphical editor?s pretty-print and gives an understandable representation of models.
The text editor is based on a new modeling framework for the Event-B method. This framework provides an EMF-based front-end to the Rodin database. Besides the advantages of EMF?s infrastructure to work with structured data models it offers an API which is similar to Rodin?s API. In addition to the meta model for core Event-B elements we have created a meta model for Event-B formulas which integrates with the core model as an extension. With these two EMF models we present a complete abstraction for the Rodin database.
To allow other plug-ins to work with the introduced text representation too, we provide a set of tools which ease its handling. They consist of a tool chain for tasks such as parsing, pretty-printing, model merging and persistence of the text representation. For the EMF formula extension the text tools offer helper classes to resolve EMF formula models from Event-B formulas in Rodin database format.
Advised By
Michael Leuschel, Jens Bendisposto
Download: PDF