Difference between revisions of "User:Nicolas/Collections/ADVANCE D3.4 Language extension"

From Event-B
Jump to: navigation, search
(Motivations / Decisions)
(Motivations / Decisions)
Line 17: Line 17:
 
** RealTheory project: including theory of Real.
 
** RealTheory project: including theory of Real.
  
Also it includes three simple Event-B models that use some of the theories:  
+
Also it includes three Event-B models that use these theories:  
 
** Data project: using SUMandPRODUCT theory  
 
** Data project: using SUMandPRODUCT theory  
 
** Queue project: using Seq theory
 
** Queue project: using Seq theory

Revision as of 15:20, 20 October 2014

Overview

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 plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component 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 plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.

Motivations / Decisions

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. The Theory plug-in 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 5 months:

  • Two versions of the Theory plug-in is released. [1] The releases include several bug fixes. The latest release (2.0.2) is considered as a stable release for Rodin v2.8.
  • A set of standard theories and some models using these theories are developed . The standard library of the theories is available to download here. 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 Event-B models that use these theories:

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

Available Documentation

Pre-studies (states of the art, proposals, discussions):

  • Proposals for Mathematical Extensions for Event-B.[2]
  • Mathematical Extension in Event-B through the Rodin Theory Component.[3]
  • Generic Parser's Design Alternatives.[4]

Technical details (specifications):

  • Mathematical_Extensions wiki page.[5]
  • Constrained Dynamic Lexer wiki page.[6]
  • Constrained Dynamic Parser wiki page.[7]
  • Theory plug-in wiki page.[8]

User's guides:

  • Theory Plug-in User Manual.[9]

Conclusion

TODO

References