imported>Asiehsalehi |
imported>Pascal |
| Line 1: |
Line 1: |
| − | Return to [[Rodin Plug-ins]]
| + | == Introduction == |
| | + | The purpose of this page is to provide a template to define the common content for all sections of the DEPLOY Deliverable D23 (Model Construction and Analysis Tool II), as mentioned in the [http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d103646/D23_Writing_Plan.pdf writing plan] for this document. |
| | | | |
| − | See also [[Theory Release History]]
| + | This template takes into consideration the review feedback for the DEPLOY Deliverable D6 (Model Construction and Analysis Tool I). |
| | | | |
| − | 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.
| + | == Template == |
| | + | For each item covered in this document (see the writing plan), a section shall be created to provide a description of work and describe the role of partners during the passed year. |
| | | | |
| − | ===Motivation===
| + | More precisely, each section shall give an overview of the contribution, some references, and some justifications for the decisions. |
| − | 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.
| + | === Overview === |
| | | | |
| − | ===Overview=== | + | === Motivations === |
| − | The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
| + | This paragraph shall indicate the state before the work and the motivation for each tool extension and improvements. |
| − | 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.
| + | In many cases the motivation will be to improve ease of use by industrial partners. |
| | | | |
| − | === Installation & Update === | + | === Design Decisions === |
| | | | |
| − | 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.
| + | === Planning === |
| | + | This paragraph shall give the current version of the feature, describe the tasks which have already been completed and announce planned further work and deadlines (release versions of the Rodin platform). |
| | | | |
| − | ===User Manual=== | + | === Available documentation === |
| − | The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual].
| + | This paragraph shall give pointers to the available wiki pages or related publications. These documents may provide input requirements, technical details (specifications), teaching materials, or be user's guides. |
| | | | |
| − | ===Worked Examples===
| + | A distinction shall be made between documentation for developpers and documentation for end-users. |
| − | In this section, you find examples of theories and models using theories. Below is the presentation of a simple theory:
| |
| | | | |
| − | [[Image:SeqThoery.png|center|thumb|800px|'''A Simple Theory''']]
| + | === Corrective and Evolutive Maintenance === |
| | + | This paragraph describes how bugs and feature requests are reviewed, |
| | | | |
| − | You can find an example of a theory and a model using that [[Media:ProdSum.pdf|''here'']].
| + | == Formatting rules == |
| | + | In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced: |
| | + | * See §4 of [http://wiki.event-b.org/images/Llncsdoc.pdf How to Edit Your Input File] for LLNCS formatting rules. |
| | + | * Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc). |
| | + | * "plug-in" shall be preferred to "plugin". |
| | | | |
| − | ===Capabilities=== | + | == Example == |
| − | 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:
| |
| − | * [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:
| |
| − | * [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
| |
| − | | |
| − | The following two papers describe rewriting and well-definedness issues that has to be accounted for:
| |
| − | | |
| − | * [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.]
| |
| − | * [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
| |
| − | | |
| − | | |
| − | [[Category:Plugin]]
| |
| − | [[Category:User documentation]]
| |
| − | [[Category:Proof]]
| |
Introduction
The purpose of this page is to provide a template to define the common content for all sections of the DEPLOY Deliverable D23 (Model Construction and Analysis Tool II), as mentioned in the writing plan for this document.
This template takes into consideration the review feedback for the DEPLOY Deliverable D6 (Model Construction and Analysis Tool I).
Template
For each item covered in this document (see the writing plan), a section shall be created to provide a description of work and describe the role of partners during the passed year.
More precisely, each section shall give an overview of the contribution, some references, and some justifications for the decisions.
Overview
Motivations
This paragraph shall indicate the state before the work and the motivation for each tool extension and improvements.
In many cases the motivation will be to improve ease of use by industrial partners.
Design Decisions
Planning
This paragraph shall give the current version of the feature, describe the tasks which have already been completed and announce planned further work and deadlines (release versions of the Rodin platform).
Available documentation
This paragraph shall give pointers to the available wiki pages or related publications. These documents may provide input requirements, technical details (specifications), teaching materials, or be user's guides.
A distinction shall be made between documentation for developpers and documentation for end-users.
Corrective and Evolutive Maintenance
This paragraph describes how bugs and feature requests are reviewed,
Formatting rules
In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced:
- See §4 of How to Edit Your Input File for LLNCS formatting rules.
- Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc).
- "plug-in" shall be preferred to "plugin".
Example
