Difference between pages "ADVANCE D3.2 Language extension" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Andy
 
Line 1: Line 1:
−
== Overview ==
+
=== The Code Generation Demonstrator Feature ===
−
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).
+
First release: 30 November 2010:
  
−
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.
+
available from: https://sourceforge.net/projects/codegenerationd/files/
  
−
== Motivations / Decisions ==
+
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.  
−
Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. Earlier versions of the Theory plugin provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory plugin became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.
 
  
−
In the past 9 months, the development of the Theory plugin resulted in the following additions:
+
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed so no further configuration should be necessary. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
  
−
* 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.
+
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
−
* 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.
 
−
* From version 2.6 of Rodin, the Theory plugin will ship as part of the core distribution. This particular decision was made given the maturity of the plugin and its potential usefulness.
 
  
−
== Available Documentation ==
+
'''A step-by-step tutorial will be available soon!!'''
−
* Pre-studies (states of the art, proposals, discussions).
 
−
** [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 ==
+
=== About the Initial Release ===
−
The Theory plugin became part of the core distribution of Rodin since version 2.6.
+
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.  
  
−
Issam Maamria will not be part of Advance after July 31, 2012.
 
  
−
== References ==
 
−
<references/>
 
  
−
[[Category:ADVANCE D3.2 Deliverable]]
+
 
 +
The SVN repository for code generation resides here:
 +
 
 +
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration
 +
 
 +
The SVN repository for tagged builds is here:
 +
 
 +
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/tags/CodeGeneration
 +
 
 +
=== Status ===
 +
* Demonstrator plug-in,
 +
** Rodin 1.3.1 version is ready for release.
 +
** Integration Testing under way.
 +
 
 +
* The Code Generation feature consists of,
 +
** a tasking Development Generator.
 +
** a tasking Development Editor (Based on an EMF Tree Editor).
 +
** a translator, from Tasking Development to Common Language Model (IL1).
 +
** a translator, from the Tasking Development to Event-B model of the implementation.
 +
** a pretty-printer for the Tasking Development.
 +
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 +
 
 +
* For the next release, our target is
 +
** Rodin 2.0 compatibility.
 +
** Introduction of sensed variables.
 +
** Event grouping in shared machines mapping to branching statements in protected objects.
 +
** Accommodation of duplicate event names in tasking developments.
 +
 
 +
 
 +
 
 +
=== Metamodels ===
 +
* In the plug-in we define several meta-models:
 +
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
 +
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
 +
** IL1 Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
 +
 
 +
=== Translation Rules ===
 +
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]

Revision as of 09:28, 30 November 2010

The Code Generation Demonstrator Feature

First release: 30 November 2010:

available from: https://sourceforge.net/projects/codegenerationd/files/

The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.

A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed so no further configuration should be necessary. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.

Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.

A step-by-step tutorial will be available soon!!

About the Initial Release

The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.



The SVN repository for code generation resides here: 

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration

The SVN repository for tagged builds is here: 

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/tags/CodeGeneration

Status

  • Demonstrator plug-in,
    • Rodin 1.3.1 version is ready for release.
    • Integration Testing under way.
  • The Code Generation feature consists of,
    • a tasking Development Generator.
    • a tasking Development Editor (Based on an EMF Tree Editor).
    • a translator, from Tasking Development to Common Language Model (IL1).
    • a translator, from the Tasking Development to Event-B model of the implementation.
    • a pretty-printer for the Tasking Development.
    • a pretty-printer for Common Language Model, which generates Ada Source Code.
  • For the next release, our target is
    • Rodin 2.0 compatibility.
    • Introduction of sensed variables.
    • Event grouping in shared machines mapping to branching statements in protected objects.
    • Accommodation of duplicate event names in tasking developments.


Metamodels

  • In the plug-in we define several meta-models:
    • CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either sequential or concurrent systems.
    • Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
    • IL1 Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.

Translation Rules

  • Tasking to IL1/Event-B translation rules [[1]]
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Language_extension&oldid=1293’