Difference between revisions of "D23 Improvements to Existing Provers"
imported>Nicolas m (→Overview) |
imported>Laurent m (→Motivations) |
||
| (17 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
= Overview = | = 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 = | = Motivations = | ||
| − | + | The motivations for improvements to existing provers can be summarized as follows: | |
| − | * | + | * Reducing proving time and effort. |
| − | : New | + | : New proof rules, both manual and automatic (e.g.., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules), have been added to discharge more proof obligations more easily. |
| − | * | + | * Reflecting corrections in prover implementations. |
| − | : | + | : The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism. |
| − | * | + | * Reducing proof storage space. |
| − | : | + | : Big proof files are difficult to handle, on the one hand by the Rodin platform (slow access), and on the other hand by users (project sharing). |
| − | : | + | : The [http://wiki.event-b.org/index.php/Proof_Purger_Interface proof purging] and [http://wiki.event-b.org/index.php/Proof_Simplification proof simplifying] mechanisms have been implemented to address this issue. |
| − | : | + | * Facilitating manual proof review or reuse. |
| − | * | + | : The [http://wiki.event-b.org/index.php/Proof_Skeleton_View proof skeleton view] allows to quickly browse through a proof. : Moreover, the provided copy/paste feature makes it possible to reuse a stored proof into a new proof. |
| − | : | + | * Improving prover API. |
| − | : | + | : The [http://wiki.event-b.org/index.php/New_Tactic_Providers tactic provider API] has been made more flexible to facilitate tactic contributions. |
| − | * | ||
| − | : | ||
| + | = 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 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 = | = Available Documentation = | ||
| Line 39: | Line 61: | ||
The following pages give useful information about prover improvements: | The following pages give useful information about prover improvements: | ||
* Prover Rules | * Prover Rules | ||
| − | : See [http://wiki.event-b.org/index.php/Inference_Rules | + | : See [http://wiki.event-b.org/index.php/Inference_Rules Inference Rules]. |
| − | : See [http://wiki.event-b.org/index.php/All_Rewrite_Rules | + | : See [http://wiki.event-b.org/index.php/All_Rewrite_Rules All Rewrite Rules]. |
* Proof Skeleton View | * Proof Skeleton View | ||
| − | : See [http://wiki.event-b.org/index.php/Proof_Skeleton_View | + | : See [http://wiki.event-b.org/index.php/Proof_Skeleton_View Proof Skeleton View]. |
* Proof Purger | * Proof Purger | ||
| − | : See [http://wiki.event-b.org/index.php/Proof_Purger_Interface | + | : See [http://wiki.event-b.org/index.php/Proof_Purger_Interface Proof Purger Interface]. |
* Prover API evolution | * Prover API evolution | ||
| − | : See [http://wiki.event-b.org/index.php/New_Tactic_Providers | + | : See [http://wiki.event-b.org/index.php/New_Tactic_Providers New Tactic Providers]. |
* Versioned Reasoners | * Versioned Reasoners | ||
| − | : See [http://wiki.event-b.org/index.php/Versioned_Reasoners | + | : See [http://wiki.event-b.org/index.php/Versioned_Reasoners Versioned Reasoners]. |
| − | |||
= Planning = | = 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 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]] | ||
Latest revision as of 11:41, 27 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
The motivations for improvements to existing provers can be summarized as follows:
- Reducing proving time and effort.
- New proof rules, both manual and automatic (e.g.., One point rule, arithmetic rules), have been added to discharge more proof obligations more easily.
- Reflecting corrections in prover implementations.
- The reasoners are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.
- Reducing proof storage space.
- Big proof files are difficult to handle, on the one hand by the Rodin platform (slow access), and on the other hand by users (project sharing).
- The proof purging and proof simplifying mechanisms have been implemented to address this issue.
- Facilitating manual proof review or reuse.
- The proof skeleton view allows to quickly browse through a proof. : Moreover, the provided copy/paste feature makes it possible to reuse a stored proof into a new proof.
- Improving prover API.
- The tactic provider API has been made more flexible to facilitate tactic contributions.
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 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 Inference Rules.
- See All Rewrite Rules.
- Proof Skeleton View
- See Proof Skeleton View.
- Proof Purger
- Prover API evolution
- See New Tactic Providers.
- Versioned Reasoners
- See Versioned Reasoners.
Planning
The above mentioned improvements were made available since release 1.1 of the platform:
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.
