Difference between revisions of "Isabelle for Rodin"

From Event-B
Jump to navigationJump to search
imported>Wohuai
(New page: The "Export to Isabelle" plug-in allows users to export proof obligations and sequents to Isabelle/HOL. Its main purpose is to help researchers analyse proof obligations in Isabelle; in t...)
 
imported>Wohuai
Line 1: Line 1:
−
The "Export to Isabelle" plug-in allows users to export proof obligations and sequents to Isabelle/HOL.
+
{| align="right"
−
Its main purpose is to help researchers analyse proof obligations in Isabelle;
+
| __TOC__
−
in the long run, it will form the basis of automated proof tactics for Event-B based on Isabelle.
+
|}
−
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].
+
 
 +
This plug-in provides an automated proof tactic based on the theorem prover [http://isabelle.in.tum.de/index.html Isabelle/HOL].
 +
It also allows users to export proof obligations to Isabelle theories for later inspection with Isabelle.
  
 
=Installation=
 
=Installation=
  
−
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'''.
+
The installation consists of the following steps:
 +
# [[#Rodin Feature|Install the Rodin feature "Isabelle for Rodin".]]
 +
# [[#Isabelle|Install Isabelle.]]
 +
# [[#HOL-EventB|Install the Isabelle logic HOL-EventB.]]
 +
# [[#Connect Isabelle to Rodin|Connect Isabelle to Rodin.]]
 +
 
 +
==Rodin Feature==
 +
 
 +
The feature can be installed using '''Rodin's software installation facilities''' and is available on '''Rodin's main update site''' (<nowiki>http://rodin-b-sharp.sourceforge.net/updates</nowiki> at time of writing) in the category '''Prover Extensions'''.
  
 
'''Please make sure that'''
 
'''Please make sure that'''
−
* the Scala update site http://download.scala-ide.org/releases/2.0.0-beta appears in the list of available software sites, and
+
* the Scala update site <nowiki>http://download.scala-ide.org/releases/2.0.0-beta</nowiki> appears in the list of available software sites, and
 
* the box "contact all update sites during install to find required software" is checked.
 
* 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.
+
==Isabelle==
−
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".
+
 
 +
Installation instructions for Isabelle can be found [http://isabelle.in.tum.de/download.html here].
 +
The main executable is ${ISABELLE_HOME}/bin/isabelle, where ${ISABELLE_HOME} is the root directory of the Isabelle installation.
 +
It may be useful to install this executable somewhere on the search path of your operating system; use "isabelle install" to do so.
 +
 
 +
==HOL-EventB==
 +
 
 +
After installing "Isabelle for Rodin", the archive containing HOL-EventB can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature*/HOL-EventB*.tgz".
 +
The update installation path refers to the place were Rodin installs plug-ins.
 +
If you have write permissions for the Rodin installation folder, the update installation path is the root directory of your Rodin installation.
 +
Otherwise, plug-ins are placed somewhere else; under Linux it may be inside "~/.eclipse".
  
−
===Prerequisites===
+
Once you have found the archive "HOL-EventB*.tgz", extract it to a location of your choice.
−
To process the generated theories, an installation of [http://isabelle.in.tum.de/download.html Isabelle2011] is required.
+
Change to the newly generated directory and invoke "isabelle make".
 +
This makes the HOL-EventB logic available to Isabelle.
 +
 
 +
==Connect Isabelle to Rodin==
 +
 
 +
Back to Rodin, go to the Preferences dialog. Navigate to the "Isabelle for Rodin" section.
 +
Make sure that the "Isabelle executable" is correctly chosen.
 +
You may enter an absolute path or a path relative to the search path or a path relative to your current work directory.
 +
Press the "Test" button to test your Isabelle installation.
 +
 
 +
'''Limitation on Windows:''' so far, it is impossible to launch Isabelle from Rodin under Windows.  
 +
More precisely, it may be possible, but it is unclear how to set the preferences.
  
 
=Usage=
 
=Usage=
  
−
The plug-in can be used to export proof obligations or the intermediate sequent of a proof attempt.
+
===Proving Proof Obligations===
 +
 
 +
To add Isabelle to the auto-tactic you have to define a parameterized tactic as follows.
 +
Search for the Auto/Post Tactic section in the Preferences dialog.
 +
Generate a new profile. As "kind" of the profile choose "Parameterized Tactic".
 +
Choose Isabelle as the tactic to be parameterized.
 +
 
 +
Back to the Auto/Post Tactic section choose the newly generated Isabelle profile as the profile used by the auto-tactic.
 +
Alternatively, you may include the Isabelle profile in another profile of the kind "Combined Tactic".
 +
 
 +
The Isabelle feature also supplies several buttons in the proof control view.
  
 
===Exporting Proof Obligations===
 
===Exporting Proof Obligations===
  
 +
You may export the proof obligations associated with a project or component (e.g. context or machine) as follows:
 
* Right-click some proof obligation(s) in the project explorer.
 
* Right-click some proof obligation(s) in the project explorer.
 
* Choose "Export to Isabelle".
 
* Choose "Export to Isabelle".
Line 30: Line 72:
 
into these folders.
 
into these folders.
 
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.
 
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 files with the proof attempts need to be renamed to the form "*.thy" before Isabelle can process them.
 
−
Separating proof obligations from proofs makes it easy to update the proof obligations without destroying the proof files.
 
  
−
===Exporting the Intermediate Sequent of a Proof Attempt===
+
The Isabelle feature also supplies a button in the proof control view to export the sequent of the current proof attempt.
  
−
The proof control provides a button "Export to Isabelle".
+
=Limitations=
−
After pressing the button, the user is prompted for a file name, where the sequent is stored.
 
  
−
=Limitations=
 
  
−
* 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.
+
Version 0.6.0 has a number of limitations.
 +
These are engineering problems that can be overcome in the future.
 +
 
 +
* Support for Windows is limited. Export of proof obligations does work. Invoking Isabelle from Rodin does not. The problem is to launch Isabelle through Cygwin from a DOS shell.
 +
* The Isabelle plug-in is slower than it could be for two reasons:
 +
** Isabelle is restarted for each proof attempt. Starting Isabelle (without starting a proof attempt) takes several seconds.
 +
** Isabelle's generic parser is used to parse the theories generated by Rodin.
 +
* The names of variables may clash with reserved keywords in Isabelle/EventB. Such a name clash may only occur with keywords that do not occur on the keyword blacklist of the plug-in. In practice, such a name clash is therefore rather unlikely (i.e., it has never been observed). The most likely consequence of such a name clash is a parse error.
 +
* The names of theories that result from exporting proof obligations may clash with the names of built-in theories of HOL or HOL-EventB. The consequence is that the generated theory cannot be loaded in Isabelle.
  
 
=News=
 
=News=
  
 
====Version 0.5.0====
 
====Version 0.5.0====
−
=====Plug-in:=====
+
=====Rodin Plug-ins:=====
 +
* integrated Isabelle as a reasoner / tactic
 +
* tested the Isabelle integration on Linux and MaxOS; the integration does not yet work on Windows
 +
* preference dialogs for configuring Isabelle
 +
* various simplifications of the user interaction
 +
 
 +
=====HOL-EventB:=====
 +
* upgrade to Isabelle2011-1
 +
* fixed a problem with printing of sequents
 +
* a command assert_finished that checks whether a proof is finished and emits an error otherwise
 +
* sensible default configuration for axe'
 +
* make use of smt_certificates so that users without Z3 can build EventB
 +
 
 +
====Version 0.5.0====
 +
=====Rodin Plug-ins:=====
 
* (incompatible) changes in translation, taking changes in HOL/Event-B into account
 
* (incompatible) changes in translation, taking changes in HOL/Event-B into account
 
* infrastructure for doing the experiments of my PhD thesis
 
* infrastructure for doing the experiments of my PhD thesis
Line 59: Line 119:
  
 
====Version 0.4.0====
 
====Version 0.4.0====
−
=====Plug-in:=====
+
=====Rodin Plug-ins:=====
 
* infrastructure for creating proof statistics with "isabelle usedir"
 
* infrastructure for creating proof statistics with "isabelle usedir"
 
* Export information about the origin of hypotheses and goals.
 
* Export information about the origin of hypotheses and goals.
Line 74: Line 134:
  
 
====Version 0.3.0====
 
====Version 0.3.0====
−
=====Plug-in:=====
+
=====Rodin Plug-ins:=====
 
* translation avoids name clashes with predefined constants
 
* translation avoids name clashes with predefined constants
 
* introduce auxiliary definitions to speed up parsing in Isabelle
 
* introduce auxiliary definitions to speed up parsing in Isabelle
Line 85: Line 145:
  
 
====Version 0.2.0====
 
====Version 0.2.0====
−
=====Plug-in:=====
+
=====Rodin Plug-ins:=====
 
* 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.   
 
* 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
 
* documentation
Line 98: Line 158:
  
 
====Version 0.1.0====
 
====Version 0.1.0====
−
=====Plug-in:=====
+
=====Rodin Plug-ins:=====
 
* initial version
 
* initial version
  

Revision as of 18:32, 25 February 2012

This plug-in provides an automated proof tactic based on the theorem prover Isabelle/HOL. It also allows users to export proof obligations to Isabelle theories for later inspection with Isabelle.

Installation

The installation consists of the following steps:

  1. Install the Rodin feature "Isabelle for Rodin".
  2. Install Isabelle.
  3. Install the Isabelle logic HOL-EventB.
  4. Connect Isabelle to Rodin.

Rodin Feature

The feature can be installed using Rodin's software installation 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.

Please make sure that

  • the Scala update site http://download.scala-ide.org/releases/2.0.0-beta appears in the list of available software sites, and
  • the box "contact all update sites during install to find required software" is checked.

Isabelle

Installation instructions for Isabelle can be found here. The main executable is ${ISABELLE_HOME}/bin/isabelle, where ${ISABELLE_HOME} is the root directory of the Isabelle installation. It may be useful to install this executable somewhere on the search path of your operating system; use "isabelle install" to do so.

HOL-EventB

After installing "Isabelle for Rodin", the archive containing HOL-EventB can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature*/HOL-EventB*.tgz". The update installation path refers to the place were Rodin installs plug-ins. If you have write permissions for the Rodin installation folder, the update installation path is the root directory of your Rodin installation. Otherwise, plug-ins are placed somewhere else; under Linux it may be inside "~/.eclipse".

Once you have found the archive "HOL-EventB*.tgz", extract it to a location of your choice. Change to the newly generated directory and invoke "isabelle make". This makes the HOL-EventB logic available to Isabelle.

Connect Isabelle to Rodin

Back to Rodin, go to the Preferences dialog. Navigate to the "Isabelle for Rodin" section. Make sure that the "Isabelle executable" is correctly chosen. You may enter an absolute path or a path relative to the search path or a path relative to your current work directory. Press the "Test" button to test your Isabelle installation.

Limitation on Windows: so far, it is impossible to launch Isabelle from Rodin under Windows. More precisely, it may be possible, but it is unclear how to set the preferences.

Usage

Proving Proof Obligations

To add Isabelle to the auto-tactic you have to define a parameterized tactic as follows. Search for the Auto/Post Tactic section in the Preferences dialog. Generate a new profile. As "kind" of the profile choose "Parameterized Tactic". Choose Isabelle as the tactic to be parameterized.

Back to the Auto/Post Tactic section choose the newly generated Isabelle profile as the profile used by the auto-tactic. Alternatively, you may include the Isabelle profile in another profile of the kind "Combined Tactic".

The Isabelle feature also supplies several buttons in the proof control view.

Exporting Proof Obligations

You may export the proof obligations associated with a project or component (e.g. context or machine) as follows:

  • Right-click some proof obligation(s) in the project explorer.
  • Choose "Export to Isabelle".

The plug-in will create "isabelle" subfolders in every involved project folder and put the translations of the proof obligations into these folders. 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 Isabelle feature also supplies a button in the proof control view to export the sequent of the current proof attempt.

Limitations

Version 0.6.0 has a number of limitations. These are engineering problems that can be overcome in the future.

  • Support for Windows is limited. Export of proof obligations does work. Invoking Isabelle from Rodin does not. The problem is to launch Isabelle through Cygwin from a DOS shell.
  • The Isabelle plug-in is slower than it could be for two reasons:
    • Isabelle is restarted for each proof attempt. Starting Isabelle (without starting a proof attempt) takes several seconds.
    • Isabelle's generic parser is used to parse the theories generated by Rodin.
  • The names of variables may clash with reserved keywords in Isabelle/EventB. Such a name clash may only occur with keywords that do not occur on the keyword blacklist of the plug-in. In practice, such a name clash is therefore rather unlikely (i.e., it has never been observed). The most likely consequence of such a name clash is a parse error.
  • The names of theories that result from exporting proof obligations may clash with the names of built-in theories of HOL or HOL-EventB. The consequence is that the generated theory cannot be loaded in Isabelle.

News

Version 0.5.0

Rodin Plug-ins:
  • integrated Isabelle as a reasoner / tactic
  • tested the Isabelle integration on Linux and MaxOS; the integration does not yet work on Windows
  • preference dialogs for configuring Isabelle
  • various simplifications of the user interaction
HOL-EventB:
  • upgrade to Isabelle2011-1
  • fixed a problem with printing of sequents
  • a command assert_finished that checks whether a proof is finished and emits an error otherwise
  • sensible default configuration for axe'
  • make use of smt_certificates so that users without Z3 can build EventB

Version 0.5.0

Rodin Plug-ins:
  • (incompatible) changes in translation, taking changes in HOL/Event-B into account
  • infrastructure for doing the experiments of my PhD thesis
  • a plug-in for generating statistics of Rodin proof tactics
HOL-EventB:
  • faster version of ebsimp, called ebsimp'
  • 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

Rodin Plug-ins:
  • 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:
  • an attribute unlifted for forward application of ebsimp
  • 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

Rodin Plug-ins:
  • 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
  • fixed pretty print problems with .>. and .\<ge>.
  • The method ebpost no longer uses assumptions in simplification to avoid simplifier loops.

Version 0.2.0

Rodin Plug-ins:
  • 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:
  • Reorganized IsaMakefile.

Version 0.1.0

Rodin Plug-ins:
  • initial version
HOL-EventB:
  • Avoid exponential blow-up by iterated bfunimage.
  • 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.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Isabelle_for_Rodin&oldid=5815’