D23 Improvements to Existing Provers: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Laurent
imported>Laurent
Heavy editing of the page
Line 1: Line 1:
= Overview =
= Overview =


All along the lifecycle of the provers, the following improvements can be achieved by:
Proving is at the core of the Rodin methodology. Therefore, it was no surprise
* Adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all).
that both industrial and academic users reported a lot of feedback on this
* Correcting bugs in implementations of existing proof rules.
topic. This feedback was provided either by mail or though the SourceForge
* Implementing new tools to help the user to do proofs.
trackers.
* 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.
Based on this feedback, several actions were taken to improve the existing
tooling for both automated and interactive proving.  Some consisted in
improving existing tools, while others needed a full design and development of
new tools (especially for visualizing and managing proofs).  Finally, an
extension of the proving framework API as been realised to allow for the
development of new plug-ins (such as the rule based prover).
 
Systerel has been in charge of existing prover improvements, with support from
ETH Zurich.  The evolution of the API has been designed in close collaboration
with University of Southampton.


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


= Motivations =
= Motivations =
Line 21: Line 28:
: Proof purging.
: Proof purging.
: Proof simplifying.
: Proof simplifying.
: Non textual database storage.
* Facilitating manual proof review or reuse.
* Facilitating manual proof review or reuse.
: Proof skeleton view.
: Proof skeleton view.
: Copy / paste from skeleton to edited proof.
: Copy / paste of partial proofs.
* Prover API evolution.
* Prover API evolution.
: New tactic provider API.
: New tactic provider API.
Line 30: Line 36:
= Choices / Decisions =
= Choices / Decisions =


A problem showed up while trying to implement a new proof rule (substitution of the domain of a total function). It required to make a reasoner able to propose several substitutions for the same function. More generally, the problem was to parameterize how a given rule shall be applied, depending on a user choice among various possible applications. Each choice should be displayed in the popup list in interactive proving.
The proving API one year ago asked that available proof commands would be
Before the improvement, a given reasoner could only propose one application. Thus, we had to define a new, more general, API. At the same time, the University of Southampton was working on Rule-Based Provers and they were also meeting difficulties dealing with the old API.
completely determined statically (at application startup). This decision had
We then started a discussion in order to define a new API that would address everyone's needs. Proposals were made on a wiki page ([http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers]) until it reached a stable state.
to be revised to allow for dynamically contributed proof commands. This change
was required not only for regular rules where several options could be
considered based on available hypotheses, but also for plugging in the rule
based prover, developed by University of Southampton.  This API extension was
fully designed and discussed through the Rodin wiki.
: See [http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers].
 
Following to the detection of incorrect proof rules implemented in the tool, a
complete review of all proof rules and their implementation has been carried
out.  Moreover, a review procedure has been defined to lower the risk that such
glitches happen again in the future.  Also, the decision to develop a rule
based prover (where rules must be formally proved before being used) will
provide greater confidence in the correctness of the prover.


During the last DEPLOY workshop (October 2009), the idea arose to change proof storage means in order to enlighten proof files, which can grow very large with current XML Rodin database storage. Possible solutions are to be investigated.
In the current setting, proof files can grow very large (in the order of tens
of megabytes).  This is partly caused by the usage of the Rodin database
mechanism for storing proofs in XML files. At the last DEPLOY workshop
(October 2009), several other options have been discussed to reduce this memory
footprint.  This issue is beging further investigated.


= Available Documentation =
= Available Documentation =
Line 55: Line 77:
The above mentioned improvements were made available since release 1.1 of the platform:
The above mentioned improvements were made available since release 1.1 of the platform:
: [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]
: [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]
In the third year of DEPLOY, most effort in the proving area will be put into:
: better management of well-definedness conditions,
: improvement to the rule based prover,
: bridging the gap with external SMT solvers,
: supporting mathematical extensions in proofs.


[[Category:D23 Deliverable]]
[[Category:D23 Deliverable]]

Revision as of 09:41, 7 January 2010

Overview

Proving is at the core of the Rodin methodology. Therefore, it was no surprise that both industrial and academic users reported a lot of feedback on this topic. This feedback was provided either by mail or though the SourceForge trackers.

Based on this feedback, several actions were taken to improve the existing tooling for both automated and interactive proving. Some consisted in improving existing tools, while others needed a full design and development of new tools (especially for visualizing and managing proofs). Finally, an extension of the proving framework API as been realised to allow for the development of new plug-ins (such as the rule based prover).

Systerel has been in charge of existing prover improvements, with support from ETH Zurich. The evolution of the API has been designed in close collaboration with University of Southampton.


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.
  • Facilitating manual proof review or reuse.
Proof skeleton view.
Copy / paste of partial proofs.
  • Prover API evolution.
New tactic provider API.

Choices / Decisions

The proving API one year ago asked that available proof commands would be completely determined statically (at application startup). This decision had to be revised to allow for dynamically contributed proof commands. This change was required not only for regular rules where several options could be considered based on available hypotheses, but also for plugging in the rule based prover, developed by University of Southampton. This API extension was fully designed and discussed through the Rodin wiki.

See http://wiki.event-b.org/index.php/New_Tactic_Providers.

Following to the detection of incorrect proof rules implemented in the tool, a complete review of all proof rules and their implementation has been carried out. Moreover, a review procedure has been defined to lower the risk that such glitches happen again in the future. Also, the decision to develop a rule based prover (where rules must be formally proved before being used) will provide greater confidence in the correctness of the prover.

In the current setting, proof files can grow very large (in the order of tens of megabytes). This is partly caused by the usage of the Rodin database mechanism for storing proofs in XML files. At the last DEPLOY workshop (October 2009), several other options have been discussed to reduce this memory footprint. This issue is beging further investigated.

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 release 1.1 of the platform:

http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes

In the third year of DEPLOY, most effort in the proving area will be put into:

better management of well-definedness conditions,
improvement to the rule based prover,
bridging the gap with external SMT solvers,
supporting mathematical extensions in proofs.
Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_Improvements_to_Existing_Provers&oldid=1963’