FAQ: Difference between revisions
imported>Mathieu m →What does mean the abbreviations showing at some proof tree nodes: change awkward title |
imported>Mathieu m Add ? |
||
| Line 1: | Line 1: | ||
== General == | == General == | ||
=== What is Event-B === | === What is Event-B? === | ||
'''Event-B''' is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/ | '''Event-B''' is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/ | ||
=== What is Rodin === | === What is Rodin? === | ||
The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. | The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. | ||
=== Where does the ''Rodin'' name come from === | === Where does the ''Rodin'' name come from? === | ||
== General Tool Usage == | == General Tool Usage? == | ||
=== How do I install external plug-ins without using Eclipse Update Manager === | === How do I install external plug-ins without using Eclipse Update Manager? === | ||
Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager. | Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager. | ||
| Line 46: | Line 46: | ||
You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release. | You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release. | ||
=== How do I generate a ''Rodin'' product from CVS === | === How do I generate a ''Rodin'' product from CVS? === | ||
In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next >}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}. | In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next >}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}. | ||
=== How do I collect debug information from the Rodin platform === | === How do I collect debug information from the Rodin platform? === | ||
You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code> | You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code> | ||
| Line 59: | Line 59: | ||
where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository]. | where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository]. | ||
=== How do I submit a patch === | === How do I submit a patch? === | ||
Good practises for patch submission are described [[How to Submit Patches|here]]. | Good practises for patch submission are described [[How to Submit Patches|here]]. | ||
=== How do I track memory leaks === | === How do I track memory leaks? === | ||
If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]]. | If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]]. | ||
[[Category:User FAQ]] | [[Category:User FAQ]] | ||
[[Category:Developer FAQ]] | [[Category:Developer FAQ]] | ||
Revision as of 17:25, 15 January 2009
General
What is Event-B?
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/
What is Rodin?
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
Where does the Rodin name come from?
General Tool Usage?
How do I install external plug-ins without using Eclipse Update Manager?
Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.
This manual installation of plug-ins is described in Installing external plug-ins manually.
The builder takes too long
Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:
- the first one is to disable the automated prover in the Preferences panel.
- the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the Obligation Explorer.
To disable the automated prover, open Rodin Preferences (menu ). In the tree in the left-hand panel, select . Then, in the right-hand panel ensure that the checkbox labelled Enable auto-tactic for proving is disabled.
To review a proof obligation, just open it in the interactive prover, then click on the review button (this is a round blue button with a R in the proof control toolbar). The proof obligation should now labelled with the same icon in the proof obligation explorer.
Modeling and Proving
Witness for Xyz missing. Default witness generated
A parameter as disappeared during a refinement. If this is intentional, you have to add a witness telling how the abstract parameter is refined.
I've added a witness for Xyz but it keeps saying "Identifier Xyz has not been defined"
As specified in the modelling language manual, the witness must be labelled by the name
of the concrete variable being concerned.
How can I do a Proof by Induction?
Induction proof will give you some tips about it.
Labels of proof tree nodes explained
- sl/dsmeans selection/deselection,
- ahmeans add hypothesis,
- ehmeans rewrite with equality from hypothesis from left to right,
- hemeans rewrite with equality from hypothesis from right to left,
- rv...tell us that this goal as been manually reviewed.
Developer FAQ
Using Rodin-CVS from eclipse consumes too much memory
You can generate a product and use it as if it was a normal release.
How do I generate a Rodin product from CVS?
In the project org.rodinp.platform, right-click on Rodin.platform and select . Choose and click on type Rodin for the Root directory, and choose the Destination directory. Then click on .
How do I collect debug information from the Rodin platform?
You may see the log in the console by appending -consoleLog to the rodin executable: rodin -consoleLog
You may add specific debug informations by setting specific options: rodin --debug options.file -consoleLog where
contains something like:
org.pluginname/debug = true org.pluginname/debug/optionaldebug = true
where optionaldebug may be found in the
file in the rodin source repository.
How do I submit a patch?
Good practises for patch submission are described here.
How do I track memory leaks?
If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks here.
