imported>Son |
imported>Nicolas |
| Line 1: |
Line 1: |
| − | == Introduction ==
| + | In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: |
| | | | |
| − | This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, the obligations can be discharged automatically. We call these added information to the model "proof hints".
| + | [[Image:PO_Commands.png]] |
| | | | |
| − | This concept of "proof hints" already exists in the form of "witness" or "theorem" in Event-B. These useful features are designed not only to help with proving the correctness of the model but also to give more information about the particular model.
| + | These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key). |
| | | | |
| − | The question is how we can decide which "features" are useful to have in the model. In principle we can go to the extreme and include the whole proof strategy into the model in order to be able to have it being discharged automatically. But this is undesirable since it will make the model difficult to understand. Having taken this into account we specify our criteria here for "proof hints".
| + | == Retry Auto Provers == |
| | | | |
| − | 1. It should help to understand the model better.
| + | As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s). |
| | | | |
| − | 2. It should improve the automatic proving rate of the model.
| + | It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s). |
| | | | |
| − | In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[Hypothesis Selection | hypothesis selection]] and proof by cases.
| + | == Recalculate Auto Status == |
| | | | |
| − | == Proof Hints ==
| + | {{TODO}} |
| | | | |
| − | The presentation for each kind of proof hints is as follows:
| + | == Proof Replay on Undischarged POs == |
| | | | |
| − | 1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.
| + | {{TODO}} |
| | | | |
| − | 2. '''Example''': an example in Event-B is presented.
| |
| | | | |
| − | 3. '''Work around''': we show a solution (rather a work-around) for the current RODIN Platform.
| |
| | | | |
| − | === Hypothesis Selection ===
| |
| − | '''Description''' This situation usually arises during interactive proofs. In this case, a developer just select some hypotheses then invoke either AtelierB P0 or newPP restricted to finish these proofs. The solution is to (somehow) give "hints" to the Proof Obligation Generator (POG) to select these hypotheses automatically when generating the corresponding proof obligation.
| |
| | | | |
| − | '''Example''' TODO
| |
| | | | |
| − | '''Workaround''' TODO
| |
| | | | |
| − | '''Proposal''' TODO
| |
| | | | |
| − | === Case distinction ===
| |
| − | '''Description''' This section discuss about a proof hint related to the case where a developer has to do a manual "proof by case", after that, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. Proving by cases are usually not done automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.
| |
| | | | |
| − | '''Example''' TODO
| |
| | | | |
| − | '''Workaround''' TODO
| |
| | | | |
| − | '''Proposal''' TODO
| + | |
| − | [[Category:Proof]]
| + | |
| − | [[Category:Work in progress]]
| + | |
| | + | |
| | + | |
| | + | |
| | + | |
| | + | |
| | + | {{TODO|Category}} |
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).
Retry Auto Provers
As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).
It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).
Recalculate Auto Status
TODO
Proof Replay on Undischarged POs
TODO
TODO: Category
