Difference between pages "D23 General Platform Maintenance" and "D23 Improvements to Existing Provers"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Nicolas
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests reported either by mail or through the appropriate trackers on SourceForge.
 
  
The noticeable new features in the main platform for the past year are listed below:
+
All along the lifecycle of the provers, the following improvements can be achieved :
* Mathematical Language V2 (releases 1.0 and upper)
+
* adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all)  
: The new version of the mathematical language is supported.
+
* correcting bugs in implementations of existing proof rules
: See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language Event-B Mathematical Language].
+
* implementing new tools to help the user do proofs
* Theorems everywhere (releases 1.0 and upper)
+
* evolving prover API to fit with the needs of prover plug-in developers
: It is possible to mix theorems and regular predicates in axioms, invariants and guards.
 
* Auto-completion (releases 1.0 and upper)
 
: When entering a predicate or expression in the Event-B machine / context editor, it is possible to type <tt>C-Space</tt> to see a list of possible identifiers that could be entered at the cursor position.
 
* Entering mathematical symbols (releases 1.1 and upper)
 
: The Rodin platform provides many more ways to enter mathematical symbols:
 
: - either type the ASCII shortcut (as in previous releases),
 
: - or type the LaTeX command (as defined in style <tt>bsymb</tt>),
 
: - or click in the ''Symbol Table'' view which displays the symbols graphically,
 
: - or directly enter the Unicode value of the symbol (for advanced users).
 
: See [http://wiki.event-b.org/index.php/Rodin_Keyboard Rodin Keyboard].
 
  
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
+
Systerel is in charge of prover improvements.
  
 
= Motivations =
 
= Motivations =
The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to WP4 partners or by advanced users during the lifecycle of the project.
 
  
Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation trackers]. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of processing it:
+
Areas of improvement for provers can be summarized as follows:
{{SimpleHeader}}
+
* reducing proving time and effort
|-
+
* providing the user with more efficient proving tools
! scope=col | Category || Partner
+
** reducing proof storage space (proof purging / simplifying / non textual database storage)
|-
+
** ease manual proof review or reuse (Proof Skeleton View with copy paste)
|AnimB || Christophe METAYER
+
* reflecting prover implementation corrections (versioning)
|-
 
|B2LaTeX || University of Southampton
 
|-
 
|Decomposition || Systerel
 
|-
 
|Event-B core || Systerel
 
|-
 
|Event-B interface || Systerel
 
|-
 
|Event-B POG || Systerel
 
|-
 
|Event-B provers || Systerel
 
|-
 
|Event-B static checker || Systerel
 
|-
 
|PRO-B || Dusseldorf
 
|-
 
|Renaming || University of Southampton
 
|-
 
|Requirements || Dusseldorf
 
|-
 
|Rodin platform || Systerel
 
|-
 
|Text editor || Dusseldorf
 
|-
 
|U2B || Southampton
 
|}
 
  
The priorities are discussed during the WP9 meetings (bi-weekly management conference call, WP9 face-to-face meetings during DEPLOY workshops).
+
Part of implemented rules and user interface features come from user feedback, mainly through SourceForge feature requests. SourceForge bugs are also an important input for corrections.
  
 
= Choices / Decisions =
 
= Choices / Decisions =
The WP9 partners have agreed on a release policy (see the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page). In particular:
 
* A new version of the Rodin platform is released every 3 months.
 
* The code is frozen during the 2 weeks preceding each release.
 
* The Eclipse versioning policy is enforced (See [http://wiki.eclipse.org/index.php/Version_Numbering Version Numbering]).
 
* A wiki page is dedicated to each release.
 
  
The main advantages, for both developers and end-users, are summarized below:
+
Proof storage in database ?
* Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
+
A more generical way to contribute tactics (New tactic provider API)
* Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
+
 
* Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.
 
  
 
= Available Documentation =
 
= Available Documentation =
The following pages give useful information about the Rodin platform releases:
+
 
* Release notes.
+
The following pages give useful information about prover improvements:
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].  
+
* Prover Rules
: More details are provided in the notes distributed with each release (eg. [http://sourceforge.net/project/shownotes.php?release_id=693928]).
+
: See [http://wiki.event-b.org/index.php/Inference_Rules http://wiki.event-b.org/index.php/Inference_Rules]
* Bugs.
+
: See [http://wiki.event-b.org/index.php/All_Rewrite_Rules http://wiki.event-b.org/index.php/All_Rewrite_Rules]
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850].
+
* Proof Skeleton View
* Feature requests.
+
: See [http://wiki.event-b.org/index.php/Proof_Skeleton_View http://wiki.event-b.org/index.php/Proof_Skeleton_View]
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672].
+
* Proof Purger
 +
: See [http://wiki.event-b.org/index.php/Proof_Purger_Interface http://wiki.event-b.org/index.php/Proof_Purger_Interface]
 +
* Prover API evolution
 +
: See [http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers]
 +
* Versioned Reasoners
 +
: See [http://wiki.event-b.org/index.php/Versioned_Reasoners http://wiki.event-b.org/index.php/Versioned_Reasoners]
  
 
= Planning =
 
= Planning =
The [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page lists in particular the upcoming releases and give the scheduled release dates.
 
 
Special efforts will be made on the following topics, which are requested by all users in an industrial context:
 
* Mathematical Extensions.
 
: Currently, the operators and basic predicates of the Event-B mathematical language supported by the Rodin platform are fixed. The purpose is to extend the platform to support user-defined data types and associated operators, including inductive data types. Users will then be able to define operators of polymorphic type as well as parameterised predicate definitions.
 
  
* Team-based Development.
+
Proof storage in database ?
: The purpose is to perform simultaneous developments.
 
: The [http://wiki.event-b.org/index.php/D23_Decomposition Decomposition plug-in] gives an answer to this requirement by allowing to cut a model in sub-models which may be handled independently. In the same manner, the [http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation EMF Compare Editor] enables the comparison of machines and contexts: it is a first step to be able to use the Rodin platform in a team environment by putting a code repository (e.g., Subversion) underneath it.
 
: In order to understand the problem properly, some usage scenarios for [http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development team-based development] and for [http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs merging proofs] have already been written. Moreover, a page has been initiated to remember the main requirements (see [http://wiki.event-b.org/index.php/Teamwork_Requirements Teamwork Requirements]). These pages provide a basis for brainstorming and further developments on the topic.
 
  
* Documentation.
 
: The purpose is to continuously increase and improve available documentation on the Wiki. It may contain requirements, pre-studies (states of the art, proposals, discussions), technical details (specifications), teaching materials (tutorials), user's guides, etc. The intended audience may be developers or end-users.
 
  
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Revision as of 10:40, 17 November 2009

Overview

All along the lifecycle of the provers, the following improvements can be achieved :

  • adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all)
  • correcting bugs in implementations of existing proof rules
  • implementing new tools to help the user do proofs
  • evolving prover API to fit with the needs of prover plug-in developers

Systerel is in charge of prover improvements.

Motivations

Areas of improvement for provers can be summarized as follows:

  • reducing proving time and effort
  • providing the user with more efficient proving tools
    • reducing proof storage space (proof purging / simplifying / non textual database storage)
    • ease manual proof review or reuse (Proof Skeleton View with copy paste)
  • reflecting prover implementation corrections (versioning)

Part of implemented rules and user interface features come from user feedback, mainly through SourceForge feature requests. SourceForge bugs are also an important input for corrections.

Choices / Decisions

Proof storage in database ? A more generical way to contribute tactics (New tactic provider API)


Available Documentation

The following pages give useful information about prover improvements:

  • Prover Rules
See http://wiki.event-b.org/index.php/Inference_Rules
See http://wiki.event-b.org/index.php/All_Rewrite_Rules
  • Proof Skeleton View
See http://wiki.event-b.org/index.php/Proof_Skeleton_View
  • Proof Purger
See http://wiki.event-b.org/index.php/Proof_Purger_Interface
  • Prover API evolution
See http://wiki.event-b.org/index.php/New_Tactic_Providers
  • Versioned Reasoners
See http://wiki.event-b.org/index.php/Versioned_Reasoners

Planning

Proof storage in database ?