Difference between pages "New Tactic Providers" and "Proof Obligation Commands"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m (Page bootstrap)
 
imported>Nicolas
 
Line 1: Line 1:
−
The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
+
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
  
−
=== Proposed Framework ===
+
[[Image:PO_Commands.png]]
  
−
public interface ITacticProvider2 {
+
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).
−
    List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
 
−
                                                    IProofTreeNode node,
 
−
                                                    Predicate hyp,
 
−
                                                    String globalInput);
 
−
}
 
  
 +
== Retry Auto Provers ==
  
−
public interface ITacticApplication {
+
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).
−
    void apply(String[] inputs, String globalInput, IProgressMonitor monitor);
 
−
}
 
  
 +
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).
  
−
public interface IPositionApplication  extends ITacticApplication {
+
== Recalculate Auto Status ==
−
    Point getHyperlinkBounds();
 
−
    String getHyperlinkLabel();
 
−
}
 
  
−
public interface IPredicateApplication extends ITacticApplication {
+
{{TODO}}
−
    Image getIcon();
+
 
−
    String getTip();
+
== Proof Replay on Undischarged POs ==
−
}
+
 
 +
{{TODO}}
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
{{TODO|Category}}

Revision as of 16:56, 4 March 2010

In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:

PO Commands.png

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=New_Tactic_Providers&oldid=6559’