Plug-in Tutorial

>next: Introduction

Tutorial for the extension of the Rodin platform by plugin addition

This tutorial is problem solving oriented. In a first part, we will focus on Rodin extensions to develop a plugin for Probabilistic Termination and Qualitative Reasoning. In a second part, we will study specific problem cases and extend Rodin to solve them. More details can be found in the Introduction.

Outline

• Introduction

First part How to extend the UI?

• 1 Creating our plug-in
• 2 Adding elements to the database (Extending the database)
• 3 Adding elements in the Rodin structured editor (Extending the structured editor)
• 4 Adding elements to the Event-B explorer (Extending the navigator)
• 5 Displaying elements in the Pretty Print Page (Extending the pretty printer)
• 6 Documenting our plug-in (Providing Eclipse Help contents)

Second part:

• 7 Enforcing rules on newly added elements (Extending the static checker)
• 8 Generating proof obligations (Extending the Proof Obligation Generator)
• 9 Adding new reasoners

Projects

The archives of the projects built in this tutorial are available here: // FIXME. Add the links to the .zip files here.

• Help.zip, which will be needed in section XXX.

>next: Introduction