Difference between pages "ADVANCE D3.2 Improvement of automated proof" and "ADVANCE D3.2 Language extension"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Im06r
 
Line 1: Line 1:
−
= Overview =
+
== Overview ==
−
In an Event-B development, more than 60% of the time is spent on proofs. That explains why all users are naturally keen for the proofs to be as automatic as possible and why the automated prover enhancement was a continuous task since the birth of the Rodin platform.
+
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).  
−
Enhancing the automated prover can be achieved by core platform refactorings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as external provers (e.g. the SMT solvers).<br>
 
−
From the core platform point of view, and within the ten first month of ADVANCE, it consisted into two tasks: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. The user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br>
 
−
From an external point of view, the SMT Solver Integration plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. It is maintained in the time frame of ADVANCE, and increases the rate of automatically discharged proof obligations.
 
  
−
= Motivations / Decisions =
+
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.
−
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in a unappropriate order. Since Rodin 2.4, a new tactic combinator 'Attempt after Lasso' is available in auto tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to share or backup this profile thus increasing the number of automatic proofs for a given proof pattern.
 
  
−
Two main reasons mainly motivated the integration of SMT solvers into the Rodin platform. Firstly, to allow Rodin to benefit from the know capacity of such solvers in the field of arithmetics. Secondly, to extract some useful informations from the proofs that these solvers produce such as unsatisfiable cores, in order to significantly decrease the proving time of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.
+
== Motivations / Decisions ==
 +
In the past 9 months, the development of the Theory plugin resulted in the following additions:
  
−
= Available Documentation =
+
* 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.  
−
A page<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref> concerning tactic profiles is available in the user manual.<br>
+
* 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.
−
A page<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref> is dedicated to the SMT Solver integration plug-in on the Event-B wiki.
+
* 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.
  
−
= Planning =
+
== Available Documentation ==
−
Enhancement of the automated proof will continue as long as Rodin is maintained. This will be mainly be achieved by the implementation of the remaining missing rewriting<ref>http://wiki.event-b.org/index.php/All_Rewrite_Rules</ref> and inference rules<ref>http://wiki.event-b.org/index.php/Inference_Rules</ref> that have already been documented, and by the addition of new ones.
+
* 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'']
  
−
Maintenance of the SMT solver integration plug-in will be ensured within the time frame of ADVANCE.
+
== Planning ==
 +
The Theory plugin became part of the core distribution of Rodin since version 2.6.
  
−
= References =
+
Issam Maamria will not be part of Advance after July 31, 2012.
 +
 
 +
== References ==
 
<references/>
 
<references/>
  
 
[[Category:ADVANCE D3.2 Deliverable]]
 
[[Category:ADVANCE D3.2 Deliverable]]

Revision as of 15:48, 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.
  • 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.

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Improvement_of_automated_proof&oldid=218’