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.