Difference between revisions of "ADVANCE D3.2 Language extension"

From Event-B
Jump to navigationJump to search
imported>Im06r
imported>Im06r
Line 7: Line 7:
 
In the past 9 months, the development of the Theory plugin resulted in the following additions:
 
In the past 9 months, the development of the Theory plugin resulted in the following additions:
  
* Support for polymorphic theorems in proofs:  
+
* 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.
* Added Support of Axiomatic Definitions:
+
* 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.
  
 
== Available Documentation ==
 
== Available Documentation ==

Revision as of 15:46, 23 June 2012

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 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.

Motivations / Decisions

In the past 9 months, the development of the Theory plugin resulted in the following additions:

  • 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.
  • 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.

Available Documentation

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