Difference between pages "Theory Plug-in" and "Theory Release History"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Asiehsalehi
 
 
Line 1: Line 1:
Return to [[Rodin Plug-ins]]
+
Back to [[Theory Plug-in]].
  
See also [[Theory Release History]]
+
Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.
  
The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.
+
===News===
 +
* ''22th December 2020'': [[#Version_4.0.1|Version 4.0.1]] is released. It requires Rodin 3.5.
 +
* ''19th December 2014'': [[#Version_3.0.0|Version 3.0.o]] is released. It requires Rodin 3.1.
 +
* ''10th July 2014'': [[#Version_2.0.2|Version 2.0.2]] is released. It requires Rodin 2.8.
 +
* ''24th June 2014'': [[#Version_2.0.1|Version 2.0.1]] is released. It requires Rodin 2.8.
 +
* ''30th April 2014'': [[#Version_2.0.0|Version 2.0.0]] is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
 +
* ''20th April 2012'': [[#Version_1.3.2|Version 1.3.2]] is released. It requires Rodin 2.4.
 +
* ''15th August 2011'': [[#Version_1.2|Version 1.2]] is released. It requires Rodin 2.2.2.
 +
* ''6th August 2011'': [[#Version_1.1|Version 1.1]] is released. It requires Rodin 2.2.2.
 +
* ''8th July 2011'': [[#Version_1.0|Version 1.0]] is released. It requires Rodin 2.2.
 +
* ''22nd May 2011'': [[#Version_0.8|Version 0.8]] released. It is based on Rodin 2.1.1.
 +
* ''11th April 2011'': [[#Version_0.7|Version 0.7]] released. It is based on Rodin 2.1.1.
 +
* ''6th January 2011'': [[#Version_0.6|Version 0.6]] released. It is based on Rodin 2.0.1.
 +
* ''28th October 2010'': [[#Version_0.5|Version 0.5]] released. It is based on Rodin 2.0.
  
===Motivation===
+
===Releases===
Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.
+
===== Version 4.0.1 =====
 +
''22th December 2020''
  
In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.
+
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
 +
** The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
 +
** The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
 +
** Manually applying an inference rule no longer throws a NullPointerException.
 +
** It is now possible to rename theories.
 +
** The TheoryPath creation dialog box has been simplified.
 +
* Optimizations:
 +
** The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
 +
** The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
  
===Overview===
+
===== Version 4.0.0-RC1 =====
The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
+
''10th April 2017''
Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., ''card'') and predicate operators (e.g., ''finite''). Datatypes extensions can be used to define enumerated datatypes (e.g., ''DIRECTION'') as well as inductive datatypes (e.g., ''Tree'').
 
  
The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The [http://wiki.event-b.org/images/Theory_Plugin.pdf user manual] provides a guide to developing and using theories.
+
Release target: Rodin 3.2
 +
* AST Extensions (4.0.0) Major API change.
 +
** Compatibility upgrade to Rodin 3.2
 +
** Support for get operator position for INFIX extended predicate operators.
 +
** Improve pattern matching for associative operators.
 +
* Theory plug-in Branding (0.0.1) Initial version
 +
* Theory Core (4.0.0) Internal implementation changes.
 +
** Compatibility upgrade to Rodin 3.2
 +
** Support for INFIX extended predicate operators.
 +
** Various bugs fixed.
 +
* Theory help (2.0.0) User documentations.
 +
* Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
 +
** Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
 +
* Theory Rule-based Prover (4.0.0)
 +
** Reasoners' input does not contain the proof-obligation context.
 +
** Use the current sequent's origin to get the proof-obligation context.
 +
** Bug fixed: translate formula to ensure they have the same formula factory.
 +
** Added version numbers for reasoners.
 +
** Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
 +
* Theory UI (3.0.0)
  
=== Installation & Update ===
+
===== Version 3.0.0 =====
 +
''17th December 2014''
  
The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.
+
Release target : Rodin 3.1
 +
* migration changes to Rodin 3.1
  
===User Manual===
+
===== Version 2.0.2 =====
The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual].
+
''10th July 2014''
  
===Worked Examples===
+
Release target : Rodin 2.8
In this section, you find examples of theories and models using theories. Below is the presentation of a simple theory:
+
* bug fixes.  
  
[[Image:SeqThoery.png|center|thumb|800px|'''A Simple Theory''']]
+
===== Version 2.0.1 =====
 +
''24th June 2014''
  
You can find an example of a theory and a model using that [[Media:ProdSum.pdf|''here'']].
+
Release target : Rodin 2.8
 +
* bug fixes.  
  
===Capabilities===
+
===== Version 2.0.0 =====
The Theory plug-in has the following capabilities:
+
''30th April 2014''
  
* Theory Definition:
+
Release target : Rodin 2.8
** Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
+
* Major changes in the usability.
** Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is ''card''. A predicate operator is one that "returns" a predicate, an example existing predicate operator is ''finite''.
+
* Important bug fixes.  
** Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
 
** Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
 
** Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
 
** Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
 
** Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
 
*Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.
 
Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.
 
  
===Insider Look===
+
===== Version 1.3.2 =====
The Theory plug-in partially satisfies the requirements outlined in the following document:
+
''20th April 2012''
* [http://deploy-eprints.ecs.soton.ac.uk/80/ Abrial, Jean-Raymond and Butler, Michael and Schmalz, Matthias and Hallerstede, Stefan and Voisin, Laurent. Mathematical Extensions Proposal]
 
  
A more accurate description of the implemented functionalities of the plug-in can be found in the following document:
+
Release target : Rodin 2.4
* [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
+
* Important bug fixes.
 +
* Improvement of deployment and un-deployment wizards
  
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
+
===== Version 1.2 =====
 +
''15th August 2011''
  
* [http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]
+
Release target : Rodin 2.2.2
* [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
+
* Bug fixes.  
 +
* Added capability to instantiate multiple theorems at once.
 +
* Added automatic tactic for expanding operator definitions RbPxd·
  
 +
===== Version 1.1 =====
 +
''6th August 2011''
  
[[Category:Plugin]]
+
Release target : Rodin 2.2.2
[[Category:User documentation]]
+
* Theory library first version.
[[Category:Proof]]
+
* Bug fixes.
 +
* Improved UI.
 +
 
 +
===== Version 1.0 =====
 +
''8th July 2011''
 +
 
 +
Release target : Rodin 2.2
 +
 
 +
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Improved project as well as workspace scope for mathematical and prover extensions.
 +
* Added tactic (xd) to expand all definitions.
 +
* Fixed support for polymorphic theorems.
 +
 
 +
===== Version 0.8 =====
 +
''22nd May 2011''
 +
 
 +
Release target : Rodin 2.1.1
 +
 
 +
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Added project as well as workspace scope for mathematical and prover extensions.
 +
 
 +
===== Version 0.7 =====
 +
''11th April 2011''
 +
 
 +
Bug fixes. Fixed for Rodin 2.1.1.
 +
 
 +
===== Version 0.6 =====
 +
''6th January 2011''
 +
 
 +
Minor bug fixes and improvements to theories pretty printer.
 +
 
 +
===== Version 0.5 =====
 +
''28th October 2010''
 +
 
 +
This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.
 +
 
 +
===Features Requests and Bugs===
 +
Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.

Revision as of 14:31, 22 December 2020

Back to Theory Plug-in.

Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.

News

  • 22th December 2020: Version 4.0.1 is released. It requires Rodin 3.5.
  • 19th December 2014: Version 3.0.o is released. It requires Rodin 3.1.
  • 10th July 2014: Version 2.0.2 is released. It requires Rodin 2.8.
  • 24th June 2014: Version 2.0.1 is released. It requires Rodin 2.8.
  • 30th April 2014: Version 2.0.0 is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
  • 20th April 2012: Version 1.3.2 is released. It requires Rodin 2.4.
  • 15th August 2011: Version 1.2 is released. It requires Rodin 2.2.2.
  • 6th August 2011: Version 1.1 is released. It requires Rodin 2.2.2.
  • 8th July 2011: Version 1.0 is released. It requires Rodin 2.2.
  • 22nd May 2011: Version 0.8 released. It is based on Rodin 2.1.1.
  • 11th April 2011: Version 0.7 released. It is based on Rodin 2.1.1.
  • 6th January 2011: Version 0.6 released. It is based on Rodin 2.0.1.
  • 28th October 2010: Version 0.5 released. It is based on Rodin 2.0.

Releases

Version 4.0.1

22th December 2020

Release target: Rodin 3.5

  • Bug fixes:
    • The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
    • The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
    • The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
    • Manually applying an inference rule no longer throws a NullPointerException.
    • It is now possible to rename theories.
    • The TheoryPath creation dialog box has been simplified.
  • Optimizations:
    • The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
    • The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
Version 4.0.0-RC1

10th April 2017

Release target: Rodin 3.2

  • AST Extensions (4.0.0) Major API change.
    • Compatibility upgrade to Rodin 3.2
    • Support for get operator position for INFIX extended predicate operators.
    • Improve pattern matching for associative operators.
  • Theory plug-in Branding (0.0.1) Initial version
  • Theory Core (4.0.0) Internal implementation changes.
    • Compatibility upgrade to Rodin 3.2
    • Support for INFIX extended predicate operators.
    • Various bugs fixed.
  • Theory help (2.0.0) User documentations.
  • Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
    • Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
  • Theory Rule-based Prover (4.0.0)
    • Reasoners' input does not contain the proof-obligation context.
    • Use the current sequent's origin to get the proof-obligation context.
    • Bug fixed: translate formula to ensure they have the same formula factory.
    • Added version numbers for reasoners.
    • Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
  • Theory UI (3.0.0)
Version 3.0.0

17th December 2014

Release target : Rodin 3.1

  • migration changes to Rodin 3.1
Version 2.0.2

10th July 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.1

24th June 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.0

30th April 2014

Release target : Rodin 2.8

  • Major changes in the usability.
  • Important bug fixes.
Version 1.3.2

20th April 2012

Release target : Rodin 2.4

  • Important bug fixes.
  • Improvement of deployment and un-deployment wizards
Version 1.2

15th August 2011

Release target : Rodin 2.2.2

  • Bug fixes.
  • Added capability to instantiate multiple theorems at once.
  • Added automatic tactic for expanding operator definitions RbPxd·
Version 1.1

6th August 2011

Release target : Rodin 2.2.2

  • Theory library first version.
  • Bug fixes.
  • Improved UI.
Version 1.0

8th July 2011

Release target : Rodin 2.2

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Improved project as well as workspace scope for mathematical and prover extensions.
  • Added tactic (xd) to expand all definitions.
  • Fixed support for polymorphic theorems.
Version 0.8

22nd May 2011

Release target : Rodin 2.1.1

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Added project as well as workspace scope for mathematical and prover extensions.
Version 0.7

11th April 2011

Bug fixes. Fixed for Rodin 2.1.1.

Version 0.6

6th January 2011

Minor bug fixes and improvements to theories pretty printer.

Version 0.5

28th October 2010

This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.

Features Requests and Bugs

Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.