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:

• |Archive1_After_Database_Extension.zip
• |Archive2_After_Structured_Editor_Extension.zip
• |Archive3_After_EventB_Explorer_Extension.zip
• |Archive4_After_PrettyPrinter_Extension.zip
• |Archive5_After_Help_Extension.zip
• |Archive6_After_Static_Checker_Extension.zip
• |Archive7_After_Proof_Obligation_Generator_Extension.zip
• |Archive8_After_Sequent_Prover_Extension.zip

>next: Introduction