Difference between revisions of "Plug-in Tutorial"

From Event-B
Jump to navigationJump to search
imported>Tommy
m
imported>Pascal
Line 8: Line 8:
 
==Outline==
 
==Outline==
 
* {{topic|Introduction_(How_to_extend_Rodin_Tutorial)|Introduction}}
 
* {{topic|Introduction_(How_to_extend_Rodin_Tutorial)|Introduction}}
''First part'' (Probabilistic Termination and Qualitative Reasoning Plugin):
+
 
 +
''First part'' How to extend the UI?
 
* {{topic|Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)|1 Creating our plug-in}}
 
* {{topic|Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)|1 Creating our plug-in}}
 
* {{topic|Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)|2 Contributing new elements in the Rodin database}}
 
* {{topic|Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)|2 Contributing new elements in the Rodin database}}
Line 15: Line 16:
 
* {{topic|Extending_Rodin_Pretty Print Page(How_to_extend_Rodin_Tutorial)|5 Display added elements in the Pretty Print Page}}
 
* {{topic|Extending_Rodin_Pretty Print Page(How_to_extend_Rodin_Tutorial)|5 Display added elements in the Pretty Print Page}}
 
* {{topic|Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)|6 Providing help}}
 
* {{topic|Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)|6 Providing help}}
 +
 +
''Second part'':
 
* {{topic|Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|7 Extending the Static Checker}}
 
* {{topic|Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|7 Extending the Static Checker}}
 
* {{topic|Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial)|8 Extending the Proof Obligation Generator}}
 
* {{topic|Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial)|8 Extending the Proof Obligation Generator}}
 
+
* {{topic|Adding_Reasoners(How_to_extend_Rodin_Tutorial)|9 Adding reasoners}}
''Second part'' (Various problem solvings):
 
*
 
*
 
*
 
  
 
==Projects==
 
==Projects==

Revision as of 12:22, 25 August 2010

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

First part How to extend the UI?

Second part:

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.