D23 Improvements to Existing Provers

From Event-B
Revision as of 10:40, 17 November 2009 by imported>Nicolas (→‎Overview)
Jump to navigationJump to search

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 ?