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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Son
 
Line 1: Line 1:
{{Navigation|Previous= [[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)]] | 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 see how to create proof obligations to discharge for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked the machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator takes statically checked files in input. One will notice that the provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand well the previous part of this tutorial, as we will not repeat all the ideas shared by the both processes.
+
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 here is "'''What needs to be mathematically proved with those newly added elements in hands?'''".
 
  
We will study here, the case of the BNF proof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
+
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".
* remove the FIN PO which is generated by default,
 
* add our new BNF PO.
 
 
=== Principles ===
 
  
1. To extend the proof obligation generator (POG) in order to add some proof obligations that one has to discharge, one has to '''define a proof obligation processor module''' using the extension point : <tt>org.eventb.core.pogModuleTypes</tt>.<br>
+
1. It should help to understand the model better.
2. Then , one has to '''set up a configuration''' involving those modules and giving them a hierachy. This is done exactly the same way as for creating a static checker configuration.<br>
 
3. Finally, it is needed to '''add this POG configuration''' to the default one, so the proof obligation generation can be performed.<br>
 
  
 +
2. It should improve the automatic proving rate of the model.
  
We want here to show how to generate one proof obligation. We will add the PO named ''BFN'' to ensure that the bound is a natural number or finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default FIN proof obligation which is generated if a convergent event (with the associated variant) is present in the model. If a probabilistic event is in the machine, we want to create our ''BFN'' PO, thus we have to remove the FIN PO.
+
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.
  
In step 1, we will explain how to create our PO ''BFN'' using informations in the state repository that we will add in step 2, so in step 3 we could create a filter to remove the PO ''FIN'' if our machine contains a probabilistic event.
+
== Proof Hints ==
  
=== Step 1 : Adding POG modules ===
+
The presentation for each kind of proof hints is as follows:
  
As we know that the POG takes its input from the static checker, the presence of a statically checked bound (ISCBound) in the statically checked model, means that one aims to prove the probabilistic convergence of this model. Thus, this information shall be shared throught our hierachy of POG modules, as it triggers the operations they could perform.
+
1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.
  
We will anticipate using this information (stored in a <tt>IPOGState</tt>) to create the ''BFN'' proof obligation :
+
2. '''Example''': an example in Event-B is presented.
  
From the extension point <tt>org.eventb.core.pogModuleTypes</tt>, create a <tt>processorModule</tt> extension to implement our first PO generation process using a POG processor :<br>
+
3. '''Work around''': we show a solution (rather a work-around) for the current RODIN Platform.
As for a static checker module,<br>
 
1. give the module an id (here fwdMachineBoundModule),<br>
 
2. a human readable name (here "Machine POG Forward Bound Module"),<br>
 
3. register a parent in the hierarchy of modules (here we used the machine POG module of the Event-B POG : <tt>org.eventb.core.machineModule</tt>),<br>
 
4. create a class for this module.(here we created the class <tt>fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule</tt>).
 
  
The above module should share (this is done by <tt>repository.setState()</tt>), at its initialisation, an <tt>IMachineBoundInfo</tt> state that we will implement in step 2.
+
=== 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.
  
@Override
+
'''Example''' Consider the following Event-B model
public void initModule(IRodinElement element,IPOGStateRepository repository, IProgressMonitor monitor) throws CoreException {
 
repository.setState(createMachineBoundInfo(element, repository));
 
}
 
 
private IMachineBoundInfo createMachineBoundInfo(IRodinElement element, IPOGStateRepository repository) throws CoreException {
 
final IRodinFile machineFile = (IRodinFile) element;
 
final ISCMachineRoot root = (ISCMachineRoot) machineFile.getRoot();
 
final ISCBound[] bounds = root.getChildrenOfType(ISCBound.ELEMENT_TYPE);
 
if (bounds.length != 1) {
 
return new MachineBoundInfo();
 
}
 
final ISCBound scBound = bounds[0];
 
final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
 
final Expression expr = scBound.getExpression(typeEnv.getFormulaFactory(), typeEnv);
 
return new MachineBoundInfo(expr, scBound);
 
}
 
Where <tt>MachineBoundInfo</tt> will be our class representing the state for the bound of the traversed machine.
 
  
To use a registered state of the repository, one can use
+
[[Image:var-hypsel.png]]        [[Image:inv-hypsel.png]]
repository.getState(IStateType<? extends IPOGState> stateType)
 
  
As we suppose the MachineBoundInfo to be a state available after our module is initialized, we will here use :
+
[[Image:init-hypsel.png]]        [[Image:set-hypsel.png]]
final IMachineBoundInfo machineBoundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
 
  
Sub-modules of our module <tt>fwdMachineBoundFinitenessModule</tt> can use this state freely from the repository using the above invocation.
+
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).
What we want to do is creating a ''BFN'' PO if the bound expression is not trivially finite. A trivially finite expression is an integer expression or derived from a boolean type.
+
[[Image:set-hypSel0_1-INV.png]]
  
Here is the code that makes those checkings :
+
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]]
  
private boolean mustProveFinite(Expression expr, FormulaFactory ff) {
+
'''Workaround''' Currently, given and event '''evt''' and invariant '''inv''', the invariant preservation proof obligation '''evt/inv/INV''' generated with the following hypotheses automatically selected;
final Type type = expr.getType();
 
if (type.equals(ff.makeIntegerType()))
 
return false;
 
if (derivedFromBoolean(type, ff))
 
return false;
 
return true;
 
}
 
  
private boolean derivedFromBoolean(Type type, FormulaFactory ff) {
+
* The invariant '''inv'''
if (type.equals(ff.makeBooleanType()))
 
return true;
 
final Type baseType = type.getBaseType();
 
if (baseType != null)
 
return derivedFromBoolean(baseType, ff);
 
if (type instanceof ProductType) {
 
final ProductType productType = (ProductType) type;
 
return derivedFromBoolean(productType.getLeft(), ff) && derivedFromBoolean(productType.getRight(), ff);
 
}
 
return false;
 
}
 
  
Here is the corresponding code that generates the PO ''BFN'' put into the process() method of our module :
+
* The guard of the event '''evt'''
  
final IMachineBoundInfo machineBoundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
+
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
  final ISCBound scBound = machineBoundInfo.getBound();
+
[[Image:new-set-hypsel.png]]
final Expression expr = machineBoundInfo.getExpression();
 
final FormulaFactory ff = repository.getFormulaFactory();
 
final IPOGSource[] sources = new IPOGSource[] { makeSource(IPOSource.DEFAULT_ROLE, scBound.getSource()) };
 
final IPORoot target = repository.getTarget();
 
final IMachineHypothesisManager machineHypothesisManager = (IMachineHypothesisManager) repository.getState(IMachineHypothesisManager.STATE_TYPE);
 
 
// if the finitness of bound is not trivial
 
// we generate the PO
 
if (mustProveFinite(expr, ff)) {
 
final Predicate finPredicate = ff.makeSimplePredicate(Formula.KFINITE, expr, null);
 
createPO(target, "BFN",
 
POGProcessorModule.makeNature("Finiteness of bound"),
 
machineHypothesisManager.getFullHypothesis(),
 
makePredicate(finPredicate, scBound.getSource()), sources,
 
machineHypothesisManager.machineIsAccurate(), monitor);
 
  
Add this module to the configuration created for the static checker by creating an extension <tt>pogModule</tt>.
+
Note that the extra (theorem) guard can be removed in the further refinement without generating any new proof obligation.
  
=== Step 2 : creating the support for sharing bound informations among POG sub-modules ===
+
=== 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.
  
We will here create the extension storing the information about the statically checked bound which we want available through sub-modules.
+
'''Example''' Consider the following Event-B model
To do this : add the <tt>org.eventb.core.pogStateTypes</tt> extension point to our plugin.
 
The create an extension <tt>stateType</tt> :<br>
 
- id : machineBoundInfo<br>
 
- name : POG Machine Bound Info<br>
 
- class a new class that will implement the interface described below.<br>
 
  
We want three methods to be available in this interface :
+
[[Image:casesplit.png]]
* getExpression() to retrieve the expression of the bound,
 
* getBound() to retrieve the statically checked bound,
 
* hasMachineBound() telling if the currently processed machine has a bound or not.
 
  
Here is the interface <tt>IMachineBoundInfo</tt> one has to create:
+
Consider the proof obligation '''set/case0_1/INV''' (Here all hypotheses, including those hidden are shown)
  
public interface IMachineBoundInfo extends IPOGState {
+
[[Image:set-case0_1-INV.png]]
 
final static IStateType<IMachineBoundInfo> STATE_TYPE = POGCore.getToolStateType(QualProbPlugin.PLUGIN_ID + ".machineBoundInfo");
 
 
/**
 
* Returns the parsed and type-checked bound expression, or <code>null</code>
 
* if the machine does not have a bound.
 
*
 
* @return the parsed and type-checked bound expression, or <code>null</code>
 
* if the machine does not have a bound
 
*/
 
Expression getExpression();
 
 
/**
 
* Returns a handle to the bound, or <code>null</code> if the machine does not have a bound.
 
*
 
* @return a handle to the bound, or <code>null</code> if the machine does not have a bound
 
*/
 
ISCBound getBound();
 
 
/**
 
* Returns whether the machine has a bound.
 
*
 
* @return whether the machine has a bound
 
*/
 
boolean machineHasBound();
 
 
}
 
  
and here is its implementation class :
+
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>.
  
public class MachineBoundInfo implements IMachineBoundInfo {
+
'''Workaround''' To capture the effect of doing '''proof by cases''', we split the original event '''set''' into two different events as follows
 
private final Expression boundExpression;
 
private final ISCBound bound;
 
  private boolean immutable;
 
 
/**
 
* Constructor
 
*/
 
public MachineBoundInfo(final Expression expression, final ISCBound bound) {
 
this.boundExpression = expression;
 
this.bound = bound;
 
immutable = false;
 
}
 
 
/**
 
* Constructor with no bound attached
 
*/
 
public MachineBoundInfo() {
 
this.boundExpression = null;
 
this.bound = null;
 
immutable = false;
 
}
 
 
@Override
 
public String toString() {
 
return boundExpression == null ? "null" : boundExpression.toString();
 
}
 
 
 
public Expression getExpression() {
 
return boundExpression;
 
}
 
 
public ISCBound getBound() {
 
return bound;
 
}
 
 
public IStateType<?> getStateType() {
 
return IMachineBoundInfo.STATE_TYPE;
 
}
 
 
public boolean machineHasBound() {
 
return boundExpression != null;
 
}
 
 
@Override
 
public void makeImmutable() {
 
immutable = true;
 
}
 
 
@Override
 
public boolean isImmutable() {
 
return immutable;
 
}
 
 
}
 
  
=== Step 3 : Removing a PO ===
+
[[Image:new-set-evts.png]]
  
To remove a PO, one has to create a filter module. This follows the same way as what is done for the static checker. After a small search in the package <tt>org.eventb.internal.core.pog.modules</tt>, we identify that the module responsible of creating the ''FIN'' PO is actually <tt>FwdMachineVariantModule</tt>. The goal is here to register our filter as a submodule of <tt>FwdMachineVariantModule</tt> that will prevent it to create the ''FIN'' PO.
+
[[Category:Proof]]
 
+
[[Category:Work in progress]]
The code is really simple... first one has to check if the model contains a probabilistic event, which means that we want to override the ''FIN'' PO that will be created by default,
 
and then, in the filter, one has to search from the generated PO if one corresponds to ''FIN'' by searching inside PO names and reject it.
 
 
 
1. give the module an id (here finPORejectingModule),<br>
 
2. a human readable name (here "Machine POG Filter FIN PO Rejecting Module"),<br>
 
3. register a parent in the hierarchy of modules (here we used the variant POG module of the Event-B POG that creates the POG we want to suppress: <tt>org.eventb.core.fwdMachineVariantModule</tt>),<br>
 
4. create a class for this module.(here we created the class <tt>fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule</tt>).
 
 
 
 
 
 
 
 
 
 
 
{{Navigation|Previous= [[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
 
 
 
[[Category:Developer documentation|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Tutorial|*Index]]
 

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