Difference between pages "Export to Isabelle" and "FAQ"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Wohuai
m
 
imported>Laurent
(→‎General: Added topic on difference between event-B and classical B)
 
Line 1: Line 1:
−
The "Export to Isabelle" plug-in allows users to export proof obligations and sequents to Isabelle/HOL.
+
== General ==
−
Its main purpose is to help researchers analyse proof obligations in Isabelle;
+
=== What is event-B? ===
−
in the long run, it will form the basis of automated proof tactics for Event-B based on Isabelle.
+
'''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/
−
The embedding of Event-B's logic in Isabelle/HOL is sound with respect to the semantics described in [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf].
 
  
−
=Installation=
+
=== What is the difference between event-B and the B method? ===
  
−
The plug-in can be installed using '''Rodin's update facilities''' and is available on '''Rodin's main update site''' (http://rodin-b-sharp.sourceforge.net/updates at time of writing) in the category '''Prover Extensions'''.
+
Event-B is derived from the {http://en.wikipedia.org/wiki/B-Method B method}. Both notations have the same {http://en.wikipedia.org/wiki/Jean-Raymond_Abrial inventor}, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose.  The B method is devoted to the development of ''correct by construction'' software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).
  
−
'''Please make sure that'''
+
Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).  
−
* the Scala update site http://download.scala-ide.org/update-current appears in the list of available software sites, and
 
−
* the box "contact all update sites during install to find required software" is checked.
 
  
−
The '''EventB Isabelle theory''' introduces Event-B's operators and binders and some proof tactics.
+
=== What is Rodin? ===
−
It is shipped with the plug-in and can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature*/HOL-EventB*.tgz".
+
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.
  
−
===Prerequisites===
+
=== Where does the ''Rodin'' name come from? ===
−
To process the generated theories, an installation of [http://isabelle.in.tum.de/download.html Isabelle2011] is required.
 
  
−
=Usage=
+
The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” .  Rodin is also the name of a famous French [http://en.wikipedia.org/wiki/Auguste_Rodin sculptor], one of his most famous work being the [http://en.wikipedia.org/wiki/The_Thinker Thinker].
  
−
The plug-in can be used to export proof obligations or the intermediate sequent of a proof attempt.
+
== General Tool Usage? ==
  
−
===Exporting Proof Obligations===
+
=== 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.
  
−
* Right-click some proof obligation(s) in the project explorer.
+
This manual installation of plug-ins is described in ''[[Installing external plug-ins manually]]''.
−
* Choose "Export to Isabelle".
 
  
−
The plug-in will create "isabelle" subfolders in every involved project folder and put the translations of the proof obligations
+
=== The builder takes too long ===
−
into these folders.
+
Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:
−
For every component (context or machine) two theory files will be generated: one storing the selected proof obligations of that component and the other one containing proof attempts.
+
* the first one is to disable the automated prover in the Preferences panel.
−
The files with the proof attempts need to be renamed to the form "*.thy" before Isabelle can process them.
+
* the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
−
Separating proof obligations from proofs makes it easy to update the proof obligations without destroying the proof files.
+
Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.
  
−
===Exporting the Intermediate Sequent of a Proof Attempt===
+
To disable the automated prover, open Rodin <tt>Preferences</tt> (menu {{menu|Window > Preferences...}}).  In the tree in the left-hand panel, select {{menu|Event-B > Sequent Prover > Auto-tactic}}. Then, in the right-hand panel ensure that the checkbox labelled <tt>Enable auto-tactic for proving</tt> is disabled.
  
−
The proof control provides a button "Export to Isabelle".
+
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 event-B explorer.
−
After pressing the button, the user is prompted for a file name, where the sequent is stored.
 
  
−
=Limitations=
+
===What are the ASCII shortcuts for mathematical operators===
  
−
* Names of variables may clash with names of reserved keywords in Isabelle, which leads to parse errors. Similarly, names of components may clash with the name of some built-in theory of HOL.
+
The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path {{menu|Event-B Keyboard User Guide > Getting Started > Special Combos}}.
  
−
=News=
+
This page is also available in the dynamic help system.  The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors.  To start the dynamic help, click {{menu|Help > Dynamic Help}}, then click {{menu|All Topics}} and select the page in the tree.
  
−
====Version 0.5.0====
+
== Modeling and Proving==
−
=====Plug-in:=====
+
=== Witness for {{Ident|Xyz}} missing. Default witness generated ===
−
* (incompatible) changes in translation, taking changes in HOL/Event-B into account
+
A parameter as disappeared during a refinement. If this is intentional, you have to add a [[Witnesses (Modelling Language)|witness]] telling how the abstract parameter is refined.
−
* infrastructure for doing the experiments of my PhD thesis
 
−
* a plug-in for generating statistics of Rodin proof tactics
 
  
−
=====HOL-EventB:=====
+
=== Identifier {{ident|Xyz}} should not occur free in a witness ===
−
* faster version of ebsimp, called ebsimp'
+
You refer to {{ident|Xyz}} in a witness predicate where {{ident|Xyz}} is a disappearing abstract variable or parameter which is not set as the witness label.
−
* axe, a smart combination of simp, clarify, safe, smt, metis, auto, and force
 
−
* tuning
 
−
* refactoring of EventB
 
−
* cleanup of EventB: added missing theorems stating that EventB constitutes a model of Event-B's main theory.
 
−
* changed the notation "x..y" to "x. .y", as the notation "x..y" is in conflict with, e.g., {x..y}.
 
  
−
====Version 0.4.0====
+
=== In {{event|INITIALISATION}}, I get  ''Witness {{ident|Xyz}} must be a disappearing abstract variable or parameter'' ===
−
=====Plug-in:=====
+
You should mark the variable as an ''after variable'' by using a tick. The witness label should be {{ident|Xyz'}}, and the predicate should refer to {{ident|Xyz'}} too.
−
* infrastructure for creating proof statistics with "isabelle usedir"
 
−
* Export information about the origin of hypotheses and goals.
 
−
* Export information about the underlying refines / sees / extends graph.
 
  
−
=====HOL-EventB:=====
+
=== I've added a witness for {{ident|Xyz}} but it keeps saying ''"Identifier {{ident|Xyz}} has not been defined"'' ===
−
* an attribute unlifted for forward application of ebsimp
+
As specified in the [[Witnesses (Modelling Language)|modelling language manual]], the witness must be labelled by the name {{Ident|Xyz}} of the concrete variable being concerned.
−
* Integrated Gudmund Grov's Formula_Origin theory, which stores the origin of a formula.
 
−
* Tuning.
 
−
* Fixed a parse problem with <+ and .<+..
 
−
* logging facilities
 
−
* a command "is_finished" that determines whether a proof is finished
 
−
* a command "timed_apply" -- a time bounded version of apply
 
  
−
====Version 0.3.0====
+
=== How can I do a Proof by Induction? ===
−
=====Plug-in:=====
+
[[Induction proof|This page about proof by induction]] will give you some starting tips.
−
* translation avoids name clashes with predefined constants
 
−
* introduce auxiliary definitions to speed up parsing in Isabelle
 
−
* improved proof skeletons
 
−
* infrastructure for predicate variables
 
  
−
=====HOL-EventB=====
+
=== Labels  of proof tree nodes explained ===
−
* fixed pretty print problems with .>. and .\<ge>.
+
* {{ident|ah}} means ''add hypothesis'',
−
* The method ebpost no longer uses assumptions in simplification to avoid simplifier loops.
+
* {{ident|eh}} means rewrite with ''equality from hypothesis'' from left to right,
 +
* {{ident|he}} means rewrite with ''equality from hypothesis'' from right to left,
 +
* {{ident|rv}} tell us that this goal as been manually [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Control_Window|reviewed]],
 +
* {{ident|sl/ds}} means ''selection/deselection'',
 +
* {{ident|PP}} means ''discharged by the predicate prover''
 +
* {{ident|ML}} means ''discharged by the mono lemma prover''
  
−
====Version 0.2.0====
 
−
=====Plug-in:=====
 
−
* Avoid duplication of selected hypotheses: hypotheses are now partitioned into the categories selected, deselected, and hidden. Formerly, selected hypotheses appeared both in the categories selected and visible. 
 
−
* documentation
 
−
* implemented a proof command that allows one to export the current sequent of a proof attempt
 
−
* success message after export
 
−
* Export of proof obligation can now be interrupted (granularity: proof obligation).
 
−
* display progress information during export
 
−
* implemented the infrastructure to export the sources of predicates and proof obligations
 
  
−
=====HOL-EventB:=====
+
== How to contribute? ==
−
* Reorganized IsaMakefile.
+
See the [[How_To_Contribute|How to contribute]] page.
  
−
====Version 0.1.0====
+
== Developer FAQ ==
−
=====Plug-in:=====
+
=== Using Rodin-CVS from eclipse consumes too much memory ===
−
* initial version
+
You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release.
  
−
=====HOL-EventB:=====
+
=== How do I generate a ''Rodin'' product from CVS? ===
−
* Avoid exponential blow-up by iterated bfunimage.
+
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}}.
−
* Fixed a bug in ebpre split that allowed for split on variables with assm x = \<bullet>.
 
−
* Bottom up translation (can still be improved) in ebpre.
 
−
* Translate set comprehensions to collect when possible.
 
−
* Tuning:
 
−
** iff rules for tfun, pfun, etc.
 
−
** don't unfold functional, injective, funimg
 
−
* Beautify structure of WD-conditions of partial operators (e.g., choice).
 
−
** F phi = not(WD phi --> phi)
 
−
* Refactoring translation rules for If
 
−
* Refactoring translation rules for brestrict, add T/F rules
 
−
* Systematically check for expanding rules in ebtranssimp1, use let
 
−
* Beautify precondition solving lemmas for partial operators
 
−
* Make D an abbreviation.
 
  
 +
=== 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>
  
−
[[Category:Plugin]]
+
You may add specific debug informations by setting specific options: <code>rodin --debug options.file -consoleLog</code> where {{file|options.file}} contains something like:
−
[[Category:User documentation]]
+
<pre>
 +
org.pluginname/debug = true
 +
org.pluginname/debug/optionaldebug = true
 +
</pre>
 +
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? ===
 +
Good practises for patch submission are described [[How to Submit Patches|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 [[Tracking Memory Leaks|here]].
 +
 
 +
=== How do I report a bug. ===
 +
See [[How_To_Contribute#How_do_I_report_a_bug_or_a_feature_request.3F|the ''How to contribute'' page]].
 +
 
 +
=== How do I save the models ? ===
 +
After the separation between a file ({{class|IRodinFile}}) and its root (a {{class|IInternalElement}}), that occurred in version 0.9.2, model saving is no more achievable through internal elements. Instead, you have to save the {{class|IRodinFile}}.
 +
 
 +
IInternalElement element = ...
 +
element.getRodinFile().save(...);
 +
 
 +
 
 +
 
 +
[[Category:User FAQ]]
 +
[[Category:Developer FAQ]]

Revision as of 08:06, 4 March 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 the difference between event-B and the B method?

Event-B is derived from the {http://en.wikipedia.org/wiki/B-Method B method}. Both notations have the same {http://en.wikipedia.org/wiki/Jean-Raymond_Abrial inventor}, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of correct by construction software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).

Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).

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?

The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” . Rodin is also the name of a famous French sculptor, one of his most famous work being the Thinker.

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 event-B Explorer.

To disable the automated prover, open Rodin Preferences (menu Window > Preferences...). In the tree in the left-hand panel, select Event-B > Sequent Prover > Auto-tactic. 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 event-B explorer.

What are the ASCII shortcuts for mathematical operators

The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path Event-B Keyboard User Guide > Getting Started > Special Combos.

This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click Help > Dynamic Help, then click All Topics and select the page in the tree.

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.

Identifier
Xyz
should not occur free in a witness

You refer to

Xyz

in a witness predicate where

Xyz

is a disappearing abstract variable or parameter which is not set as the witness label.

In
INITIALISATION
, I get Witness
Xyz
must be a disappearing abstract variable or parameter

You should mark the variable as an after variable by using a tick. The witness label should be

Xyz'

, and the predicate should refer to

Xyz'

too.

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

Xyz

of the concrete variable being concerned.

How can I do a Proof by Induction?

This page about proof by induction will give you some starting tips.

Labels of proof tree nodes explained

  • ah
    means add hypothesis,
  • eh
    means rewrite with equality from hypothesis from left to right,
  • he
    means rewrite with equality from hypothesis from right to left,
  • rv
    tell us that this goal as been manually reviewed,
  • sl/ds
    means selection/deselection,
  • PP
    means discharged by the predicate prover
  • ML
    means discharged by the mono lemma prover


How to contribute?

See the How to contribute page.

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 export. Choose Plug-in Development > Eclipse product and click on Next type Rodin for the Root directory, and choose the Destination directory. Then click on Finish.

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

options.file

contains something like: 

org.pluginname/debug = true
org.pluginname/debug/optionaldebug = true

where optionaldebug may be found in the

org.pluginname/.options

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.

How do I report a bug.

See the How to contribute page.

How do I save the models ?

After the separation between a file (IRodinFile) and its root (a IInternalElement), that occurred in version 0.9.2, model saving is no more achievable through internal elements. Instead, you have to save the IRodinFile. 

IInternalElement element = ...
element.getRodinFile().save(...);
Retrieved from ‘https://wiki.event-b.org/index.php?title=Export_to_Isabelle&oldid=5176’