Difference between pages "Extending the Rodin Structured Editor (How to extend Rodin Tutorial)" and "Proof Hints"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m (New page: {{Navigation|Previous= Extend the database | Up= How to extend Rodin Tutorial (Index) | Next= }} === In this ...)
 
imported>Son
 
Line 1: Line 1:
−
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
+
== Introduction ==
  
−
=== In this part ===
+
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".
−
We will use the extension points provided by the plugin <tt>org.eventb.ui</tt> to add our Probabilistic Attribute on events and the Bound Element to the Structured Editor.
 
  
−
=== Step 1 ===
+
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.
−
To structure a bit our development, we will separate the UI from the business layer.<br>
 
−
1. Create a new plugin (here <tt>fr.systerel.rodinextension.sample.ui</tt>, and this time, select "This plug-in will make contributions to the UI" as it will be indeed the case here.<br>
 
−
2. Add our business plugin (<tt>fr.systerel.rodinextension.sample</tt>) to the dependencies as well as <tt>org.eventb.ui</tt> that provides the extensions points we want to use.
 
  
−
=== Step 2 ===
+
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".
−
1. Add the extension point <tt>org.eventb.ui.editorItems</tt>
 
−
At this point, we will start to add our extensions to the structured editor.<br>
 
  
−
=== Step 3 ===
+
1. It should help to understand the model better.
−
First, let's add the probabilistic attribute to Event-B events.<br>
 
−
The probabilistic attribute can have two values : 'standard' (by default) and 'probabilistic'. Thus we need to create a 'choiceAttribute' extension.
 
−
Create a new 'choice attibute' extension :<br>
 
−
1. give a unique ID to identify this attribute in the UI plugin (such as <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>),<br>
 
−
2. in typeID, give the ID reference of the probabilistic attribute in our business plugin (here <tt>fr.systerel.rodinextension.sample.probabilistic</tt>), <br>
 
−
3. create a class (using Eclipse assist, see [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Step4]]) to manipulate this attribute, this class should implements the interface <tt>org.eventb.ui.IAttributeManipulation</tt>.
 
−
:This class should be implemented the following :
 
−
:Before doing any manipulation on
 
−
:1. getPossibleValues() should return an array of two constant values : 'standard' and 'probabilistic',
 
−
:2. // FIXME Continue here.
 
  
 +
2. It should improve the automatic proving rate of the model.
  
 +
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.
  
 +
== Proof Hints ==
  
 +
The presentation for each kind of proof hints is as follows:
  
−
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
+
1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.
  
−
[[Category:Developer documentation|*Index]]
+
2. '''Example''': an example in Event-B is presented.
−
[[Category:Rodin Platform|*Index]]
+
 
−
[[Category:Tutorial|*Index]]
+
3. '''Work around''': we show a solution (rather a work-around) for the current RODIN Platform.
 +
 
 +
=== Hypothesis Selection ===
 +
'''Description''' In order to discharge the proof obligation, the developer just selects 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''' Consider the following Event-B model
 +
 
 +
[[Image:var-hypsel.png]]        [[Image:inv-hypsel.png]]
 +
 
 +
[[Image:init-hypsel.png]]        [[Image:set-hypsel.png]]
 +
 
 +
Consider the proof obligation '''set/hypSel0_1/INV''' which states that the event '''set''' maintains invariant '''hypSel0_1''' (Here <math>\ldots</math> denotes the unselected hypotheses).
 +
[[Image:set-hypSel0_1-INV.png]]
 +
 
 +
Any provers works with only the selected hypotheses cannot discharge the above proof olbligation since the hypothesis <math>x \neq 0 \limp y \in \nat</math> is missing. The obligation with the appropriate hypothesis selection is as follows
 +
[[Image:set-hypSel0_1-INV-sel.png]]
 +
 
 +
'''Workaround''' Currently, given and event '''evt''' and invariant '''inv''', the invariant preservation proof obligation '''evt/inv/INV''' generated with the following hypotheses automatically selected;
 +
 
 +
* The invariant '''inv'''
 +
 
 +
* The guard of the event '''evt'''
 +
 
 +
In order to have the needed hypothesis selected automatically, we will add this hypothesis into the guard.  Moreover, in order to avoid changing event's behaviour, we will mark this extra guard as a theorem.  Apply this technique, the new event '''set''' is as follows
 +
[[Image:new-set-hypsel.png]]
 +
 
 +
Note that the extra (theorem) guard can be removed in the further refinement without generating any new proof obligation.
 +
 
 +
=== Case distinction ===
 +
'''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by cases" based on some condition <math>P</math>. Afterwards, 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. ''Proof by cases'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.
 +
 
 +
'''Example''' Consider the following Event-B model
 +
 
 +
[[Image:casesplit.png]]
 +
 
 +
Consider the proof obligation '''set/case0_1/INV''' (Here all hypotheses, including those hidden are shown)
 +
 
 +
[[Image:set-case0_1-INV.png]]
 +
 
 +
In order to finish the proof, a correct "proof by cases" is done to consider <math>a = 1</math> or <math>a \neq 1</math>.
 +
 
 +
'''Workaround''' To capture the effect of doing '''proof by cases''', we split the original event '''set''' into two different events as follows
 +
 
 +
[[Image:new-set-evts.png]]
 +
 
 +
[[Category:Proof]]
 +
[[Category:Work in progress]]

Revision as of 16:54, 5 March 2010

Introduction

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".

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.

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".

1. It should help to understand the model better.

2. It should improve the automatic proving rate of the model.

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 and proof by cases.

Proof Hints

The presentation for each kind of proof hints is as follows:

1. Description: A brief description of the proof hints with the situation where this can be helpful.

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 In order to discharge the proof obligation, the developer just selects 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 Consider the following Event-B model

Var-hypsel.png Inv-hypsel.png

Init-hypsel.png Set-hypsel.png

Consider the proof obligation set/hypSel0_1/INV which states that the event set maintains invariant hypSel0_1 (Here \ldots denotes the unselected hypotheses). Set-hypSel0 1-INV.png

Any provers works with only the selected hypotheses cannot discharge the above proof olbligation since the hypothesis x \neq 0 \limp y \in \nat is missing. The obligation with the appropriate hypothesis selection is as follows Set-hypSel0 1-INV-sel.png

Workaround Currently, given and event evt and invariant inv, the invariant preservation proof obligation evt/inv/INV generated with the following hypotheses automatically selected;

  • The invariant inv
  • The guard of the event evt

In order to have the needed hypothesis selected automatically, we will add this hypothesis into the guard. Moreover, in order to avoid changing event's behaviour, we will mark this extra guard as a theorem. Apply this technique, the new event set is as follows New-set-hypsel.png

Note that the extra (theorem) guard can be removed in the further refinement without generating any new proof obligation.

Case distinction

Description In order to discharge a proof obligation, the developer makes a manual "proof by cases" based on some condition P. Afterwards, 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. Proof by cases is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.

Example Consider the following Event-B model

Casesplit.png

Consider the proof obligation set/case0_1/INV (Here all hypotheses, including those hidden are shown)

Set-case0 1-INV.png

In order to finish the proof, a correct "proof by cases" is done to consider a = 1 or a \neq 1.

Workaround To capture the effect of doing proof by cases, we split the original event set into two different events as follows

New-set-evts.png

Retrieved from ‘https://wiki.event-b.org/index.php?title=Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)&oldid=6509’