Difference between pages "Single View Design" and "Theory Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Maria
 
(Add to Theory Plug-in category)
 
Line 1: Line 1:
−
==Purpose==
+
Return to [[Rodin Plug-ins]]
−
The purpose of the Single View Design is to present everything in a single view in Rodin.
 
  
−
==Specification==
+
See also [[Theory Release History]]
−
The Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] that is provided by Eclipse.
 
  
−
[[Image:MasterDetails.jpg]]
+
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.
  
−
===The Navigator===
+
===Motivation===
−
The navigator is the part on the left that contains a tree. It presents all projects and their contents. The users can choose between to ways how the machines and contexts will be presented:
+
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.
−
*A simple structure where all machines and contexts are presented on the same level
 
−
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
 
  
−
===The Details===
+
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.
−
The details part is situated on the right and may contain several tabs. The content of each tab may depend on the selection in the navigator. Currently the only tab that exists is the statistics tab. It is possible to add new custom tabs.
 
  
−
====Statistics====
+
The latest Theory plug-in is released for Rodin v2.8.
−
The statistics tab presents information about the state of the proof obligations of the selected node in the navigator.
 
  
−
==User guide==
+
===Overview===
−
===Customizing the Navigator===
+
The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
−
Click on the little triangle in the upper right corner of the navigator view and select ''Customize View''. This opens a dialog that allows you to choose ''Filters'' and ''Content''.
+
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''). Axiomatic definitions can be used to define new data types like "REAL".
  
−
[[Image:Customize.jpg]]
+
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.
  
−
====Content====
+
=== Installation & Update ===
−
Here you can choose what content should be shown in the navigator.
 
−
*'''Resources''': All projects, files and folder (keep this one checked!).
 
−
*'''Working Sets''': Allows you to see the working sets as top level elements. If you're not familiar with working sets, consult [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.user/concepts/cworkset.htm eclipse help].
 
−
*'''Simple Context Structure''': Lists all contexts of a project.
 
−
*'''Complex Context Structure''': Lists all contexts of a project. Contexts that extend another context are attached to it as children in the tree. Contexts that are seen by a machine are attached to the machine as children. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
 
−
*'''Simple Machines Structure''': Lists all machines of a project.
 
−
*'''Complex Context Structure''': Lists all machines of a project. Machines that refine another machine are attached to it as children in the tree. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
 
−
*'''Carrier Sets'''
 
−
*'''Constants'''
 
−
*'''Variables'''
 
−
*'''Axioms'''
 
−
*'''Invariants'''
 
−
*'''Theorems'''
 
−
*'''Events'''
 
−
*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.
 
  
−
Here's an example of what the same projects looks like once using the complex machine and context structure (left) and once using the simple version (right).
+
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.
  
−
[[Image:Complex.jpg]][[Image:Simple.jpg]]
+
===User Manual===
 +
The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual]. Below is the presentation of the sequence theory which its description can be found in the user manual:
  
−
====Filters====
+
[[image:SeqTheory.png|center|thumb|1500px|'''Theory of Sequence''']]
−
The filters let you choose what to hide in the navigator.
 
−
*'''File extensions''': There are various filters to hide certain types of files.
 
−
*'''All files and folders''': Hides all files and subfolders.
 
−
*'''Non Rodin Projects''': Hides all non Rodin projects. Also hides closed Rodin Projects.
 
−
*'''Closed Projects''': Hides all closed projects.
 
  
−
There are some additional filters that can be found on top of the navigator:
+
===Standard Library===
 +
In this section, you find a set of standard theories and some models using some of these theories.
  
−
[[Image:PoFilters.JPG]]
+
The standard library of the theories is available to download:
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here] for Rodin2.8 and
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.2.zip/download here] for Rodin3.1.
 +
This library includes:
 +
* BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
 +
* RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
 +
* RealTheory project: including theory of Real.
  
−
Enter a text into the field and only proof obligations containing the string will be shown. If you push the green button, all discharged proof obligations will be hidden.
+
Also it includes three simple Event-B models that use some of the theories:
 +
* Data project: using SUMandPRODUCT theory
 +
* Queue project: using Seq theory
 +
* SimpleNetwork project: using closure theory
  
−
===Statistics===
+
In order to keep the POs discharged, you need to install "Atelier B provers" as well.
−
The content displayed in the statistics tab depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.
 
  
−
It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
+
===Capabilities===
 +
The Theory plug-in has the following capabilities:
  
−
==Developer guide==
+
* Theory Definition:
−
===Extending Single View Design===
+
** 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.
−
Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] and [http://help.eclipse.org/stable/index.jsp?topic=/org.eclipse.platform.doc.isv/guide/forms_master_details.htm the Master/Details pattern]. The part on the left (the navigator) is the master part. You can add custom filters, content providers and action providers in a plug-in of your own. Add the extension <code>org.eclipse.ui.navigator.viewer</code>. There you can add viewerContentBindings and viewerActionBindings with viewerId <code>fr.systerel.explorer.navigator.view</code>. This binds your custom content, actions and filters to the navigator. The part on the right is the details part. You can add tabs of your own by extending <code>fr.systerel.explorer.masterDetails</code>.
+
** 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''.
 +
** 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.
  
−
In the picture you can see what types the nodes in the navigator have.
+
===Insider Look===
 +
The Theory plug-in partially satisfies the requirements outlined in the following document:
 +
* [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]
  
−
[[Image:Tree.jpg]]
+
A more accurate description of the implemented functionalities of the plug-in can be found in the following document:
 +
* [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
  
−
====Adding a content provider to the navigator====
+
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
−
To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineFile nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineFile</code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your navigatorContent in your viewerContentBindings.
 
  
−
<code>
+
* [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.]
−
  <extension
+
* [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
−
        point="org.eclipse.ui.navigator.navigatorContent">
 
−
      <navigatorContent
 
−
            contentProvider="example.ContentProvider"
 
−
            id="example.navigatorContent"
 
−
            labelProvider="example.LabelProvider"
 
−
            name="Example Content">
 
−
        <triggerPoints>
 
−
            <instanceof
 
−
                  value="org.eventb.core.IMachineFile">
 
−
            </instanceof>
 
−
        </triggerPoints>
 
−
      </navigatorContent>
 
−
  </extension>
 
−
</code>
 
  
−
<code>
 
−
  <extension
 
−
        point="org.eclipse.ui.navigator.viewer">
 
−
      <viewerContentBinding
 
−
            viewerId="fr.systerel.explorer.navigator.view">
 
−
        <includes>
 
−
            <contentExtension
 
−
                  pattern="example.navigatorContent">
 
−
            </contentExtension>
 
−
        </includes>
 
−
      </viewerContentBinding>
 
−
  </extension>
 
−
</code>
 
  
−
====Adding a filter to the navigator====
+
[[Category:Plugin]]
−
To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings.
+
[[Category:User documentation]]
−
 
+
[[Category:Proof]]
−
====Adding an action provider to the navigator====
+
[[Category:Theory Plug-in]]
−
To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings.
 
−
 
 
−
====Adding a tab with custom content to the details part====
 
−
To add a custom tab use  the <code>fr.systerel.explorer.masterDetails</code> extension. Add a new detailsTab and provide a class that implements <code>INavigatorDetailsTab</code>.
 
−
 
 
−
[[Category:Work in progress]]
 

Latest revision as of 14:53, 14 June 2021

Return to Rodin Plug-ins

See also Theory Release History

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.

Motivation

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.

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.

The latest Theory plug-in is released for Rodin v2.8.

Overview

The Theory plug-in is a Rodin extension that provides the facility to define mathematical extensions as well as prover extensions. 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). Axiomatic definitions can be used to define new data types like "REAL".

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 user manual provides a guide to developing and using theories.

Installation & Update

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.

User Manual

The user manual is available here: Theory User Manual. Below is the presentation of the sequence theory which its description can be found in the user manual:

Theory of Sequence

Standard Library

In this section, you find a set of standard theories and some models using some of these theories.

The standard library of the theories is available to download: 

here for Rodin2.8 and
here for Rodin3.1.

This library includes:

  • BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
  • RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
  • RealTheory project: including theory of Real.

Also it includes three simple Event-B models that use some of the theories:

  • Data project: using SUMandPRODUCT theory
  • Queue project: using Seq theory
  • SimpleNetwork project: using closure theory

In order to keep the POs discharged, you need to install "Atelier B provers" as well.

Capabilities

The Theory plug-in has the following capabilities:

  • Theory Definition:
    • 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.
    • 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.
    • 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

The Theory plug-in partially satisfies the requirements outlined in the following document:

A more accurate description of the implemented functionalities of the plug-in can be found in the following document:

The following two papers describe rewriting and well-definedness issues that has to be accounted for:

Retrieved from ‘https://wiki.event-b.org/index.php?title=Single_View_Design&oldid=14456’