Difference between revisions of "D23 Improvements to Existing Provers"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Nicolas
Line 51: Line 51:
 
= Planning =
 
= Planning =
  
−
Proof storage in database ? {{TODO}}
+
The above mentioned improvements were made available since Platform release 1.1:
−
 
+
: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes]
  
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Revision as of 14:38, 17 November 2009

Overview

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

  • 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 to do proofs.
  • Evolving the prover API to fit with the needs of prover plug-in developers.

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

Systerel is in charge of existing prover improvements. University of Southampton gave feedback for the definition of prover API evolution.

Motivations

Areas of improvement for provers can be summarized as follows:

  • Reducing proving time and effort.
New proof rules.
  • Reflecting prover implementation corrections.
Reasoner versioning.
  • Reducing proof storage space.
Proof purging.
Proof simplifying.
Non textual database storage.
  • Facilitating manual proof review or reuse.
Proof skeleton view.
Copy / paste from skeleton to edited proof.
  • Prover API evolution.
New tactic provider API.

Choices / Decisions

Proof storage in database ? TODO 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

The above mentioned improvements were made available since Platform release 1.1:

http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes
Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_Improvements_to_Existing_Provers&oldid=1958’