Difference between pages "ADVANCE D3.2 Language extension" and "AnimB install"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Christophe
 
Line 1: Line 1:
== Overview ==
+
Generally speaking, AnimB is installed and updated from within Rodin.
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).  
 
  
The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.
+
There is two  ways of installing AnimB:
 +
* for the first one (advised), you need to be connected on internet
 +
* for the second one (troubles with proxy or firewall, ...), you download the update site and install from local.
  
== Motivations / Decisions ==
+
==Begin the installation==
In the past 9 months, the development of the Theory plugin resulted in the following additions:
+
Begin the installation from the Rodin Help menu item :
 +
*Help
 +
*Software Updates
 +
*Find and Install...
 +
[[Image:step1.png|600px|center]]<br>
 +
----
 +
Select the option for new feature.<br>
 +
[[Image:step2.png|400px|center]]
 +
==Adding the AnimB update site==
 +
This screen will vary depending on the features you have installed already. <br>
 +
Click on the "New Remote Site..." button. <br>
 +
If you are behind a proxy and the Eclipse install mechanism does not work, then you can [http://www.animb.org/updatesite/AnimB.zip download] an Archived Site and then click the "New Archived Site..." button instead.
 +
[[Image:step6.png|500px|center]]<br>
 +
===Remote site===
 +
Fill in the "New Update Site" dialog with the following information and click OK.
 +
[[Image:Step7.png|300px|center]]
 +
===Archived Site===
 +
First download the [http://www.animb.org/updatesite/AnimB_V0_0_4.zip archived site] and save it on local.<br>
 +
Then click on "New Archived Site..."<br>
 +
Selected the downloaded file and click on open.
 +
[[Image:step8.png|400px|center]]
 +
Control the value field of the next dialog :
 +
[[image:step9.png|300px|center]]
  
* Support for polymorphic theorems in proofs: theorems can be used to ensure the operator and datatype definitions capture the intended understanding by the theory developer. However, requests have been made to ensure that theorems are accessible for proofs. It was decided to provide a user interface-based wizard for instantiating the type parameters in order to 'localise' the theorem based on the current sequent.  
+
==Install AnimB==
* Added support of axiomatic definitions: as of version 1.3.2 of the Theory plugin, only direct and recursive definitions for operators are possible. Requests have been made to add support for axiomatic operator definitions, which can open the door for sophisticated type definitions, e.g., the definition of REALS as an ordered ring with addition and multiplication.
+
Select the AnimB site and click on finish.
* From version 2.6 of Rodin, the Theory plugin will ship as part of the core distribution. This particular decision was made based on the maturity of the plugin as well as its popularity.
+
[[Image:Step10.png|600px|center]]
 +
----
 +
The rest is fairly straightforward.
  
== Available Documentation ==
+
[[Category:User documentation]]
* Pre-studies (states of the art, proposals, discussions).
+
[[Category:AnimB]]
** [http://deploy-eprints.ecs.soton.ac.uk/216/ ''Proposals for Mathematical Extensions for Event-B'']
 
** [http://deploy-eprints.ecs.soton.ac.uk/251/ ''Mathematical Extension in Event-B through the Rodin Theory Component'']
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives ''Generic Parser's Design Alternatives'' ]
 
** [http://wiki.event-b.org/index.php/Structured_Types ''Theoretical Description of Structured Types'']
 
* Technical details (specifications).
 
** [http://wiki.event-b.org/index.php/Mathematical_Extensions ''Mathematical_Extensions wiki page'']
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer ''Constrained Dynamic Lexer wiki page'']
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser ''Constrained Dynamic Parser wiki page'']
 
** [http://wiki.event-b.org/index.php/Theory_Plug-in ''Theory plug-in wiki page]
 
** [http://wiki.event-b.org/index.php/Records_Extension ''Records Extension Documentation on wiki'']
 
* Teaching materials (tutorials).
 
* User's guides.
 
** [http://wiki.event-b.org/images/Theory_UM.pdf ''Theory Plug-in User Manual'']
 
 
 
== Planning ==
 
The Theory plugin became part of the core distribution of Rodin since version 2.6.
 
 
 
Issam Maamria will not be part of Advance after July 31, 2012.
 
 
 
== References ==
 
<references/>
 
 
 
[[Category:ADVANCE D3.2 Deliverable]]
 

Revision as of 22:54, 3 March 2009

Generally speaking, AnimB is installed and updated from within Rodin.

There is two ways of installing AnimB:

  • for the first one (advised), you need to be connected on internet
  • for the second one (troubles with proxy or firewall, ...), you download the update site and install from local.

Begin the installation

Begin the installation from the Rodin Help menu item :

  • Help
  • Software Updates
  • Find and Install...
Step1.png



Select the option for new feature.

Step2.png

Adding the AnimB update site

This screen will vary depending on the features you have installed already.
Click on the "New Remote Site..." button.
If you are behind a proxy and the Eclipse install mechanism does not work, then you can download an Archived Site and then click the "New Archived Site..." button instead.

Step6.png


Remote site

Fill in the "New Update Site" dialog with the following information and click OK.

Step7.png

Archived Site

First download the archived site and save it on local.
Then click on "New Archived Site..."
Selected the downloaded file and click on open.

Step8.png

Control the value field of the next dialog :

Step9.png

Install AnimB

Select the AnimB site and click on finish.

Step10.png

The rest is fairly straightforward.