imported>Laurent |
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: |
| | | | |
| − | == API Proposal ==
| + | [[Image:PO_Commands.png]] |
| | | | |
| − | The current proposal consists in the following published interfaces: | + | 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). |
| | | | |
| − | public interface ITacticProvider2 {
| + | == Retry Auto Provers == |
| − | List<ITacticApplication> getPossibleApplications(IProofTreeNode node,
| |
| − | Predicate hyp,
| |
| − | String globalInput);
| |
| − | }
| |
| | | | |
| − | 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). |
| − | ITactic getTactic(String[] inputs,
| |
| − | String globalInput);
| |
| − | }
| |
| | | | |
| − | public interface IPositionApplication extends ITacticApplication {
| + | 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). |
| − | Point getHyperlinkBounds();
| |
| − | String getHyperlinkLabel();
| |
| − | }
| |
| | | | |
| − | public interface IPredicateApplication extends ITacticApplication {
| + | == Recalculate Auto Status == |
| − | Image getIcon();
| |
| − | String getTooltip();
| |
| − | }
| |
| | | | |
| − | The current extension point "proofTactics" remains unchanged.
| + | This command is related to the "auto" or "manual" PO status. This status is visible in the explorer on each PO: it is marked with a 'A' at the upper right corner of the PO icon if it was entirely discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially). |
| | | | |
| − | All those interfaces are intended to be implemented by clients.
| + | Launching 'Recalculate Auto Status' reruns the current auto prover on selected POs. The main aim of this command is to update the "auto"/"manual" status to reflect the current auto prover configuration. In case a proof was previously automatically discharged and is no more, it will be marked as manually created. |
| | | | |
| − | == Explanations ==
| + | This is intended to be used as a post-development operation to estimate the percentage of automated proofs over a changing auto prover. It is recommended to restore to the default auto provers before running this command. |
| | | | |
| − | The idea is to encapsulate in {{class|ITacticApplication}} all data needed by the UI to display and apply tactics.
| + | == Proof Replay on Undischarged POs == |
| − | Thus, an {{class|ITacticProvider2}}, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' tactic applications.
| |
| | | | |
| | + | {{TODO}} |
| | | | |
| − | Interfaces {{class|IPositionApplication}} and {{class|IPredicateApplication}} are particular application types:
| |
| | | | |
| − | * {{class|IPositionApplication}} is for tactics applied at a given position in a formula (red hyperlinks in interactive prover UI). The methods allow to override extension point data, in order to have a different text for each application in the hyperlink list. If '''null''' is returned, then default data from extension point is taken.
| |
| | | | |
| − | * {{class|IPredicateApplication}} is for tactics applied at a whole predicate, like 'Contradict Goal' or 'Contradict Hyp' (icons on the left of a predicate in interactive prover UI). The methods allow to override extension point data, in order to have a different icon and tooltip for each application in the left icon list. If '''null''' is returned, then default data from extension point is taken.
| |
| | | | |
| − | == Example ==
| |
| | | | |
| − | The following example demonstrates (part of) the implementation of a tactic using the proposed API.
| |
| − | For simplicity, a simple {{class|ITacticApplication}} is used, but a {{class|IPositionApplication}} could (should) be used instead.
| |
| − | The underlying {{class|IReasoner}} ({{class|ExampleReasoner}}) is not shown here, as it is not impacted by the proposed API.
| |
| | | | |
| − | <pre>
| |
| − | // rewrites occurrences of literal 4 into either 2+2 or 2*2
| |
| − | public class ExampleTacticProvider2 implements ITacticProvider2 {
| |
| | | | |
| − | // our own implementation of a tactic application
| |
| − | private static class ExampleApplication implements ITacticApplication {
| |
| | | | |
| − | private final IUserSupport userSupport;
| |
| − | private final Predicate hyp;
| |
| − | private final IPosition position;
| |
| − | // 2 Kinds: PLUS (2+2) and MULT (2*2)
| |
| − | private final ExampleReasoner.Kind kind;
| |
| | | | |
| − | public ExampleApplication(IUserSupport userSupport, Predicate hyp, IPosition position, Kind kind) {
| |
| − | this.userSupport = userSupport;
| |
| − | this.hyp = hyp;
| |
| − | this.position = position;
| |
| − | this.kind = kind;
| |
| − | }
| |
| | | | |
| − | public void apply(String[] inputs, String globalInput, IProgressMonitor monitor) {
| |
| − | try {
| |
| − | // ExampleReasoner implements IReasoner and rewrites literal 4
| |
| − | // at given position into:
| |
| − | // . 2+2 if input.kind is PLUS
| |
| − | // . 2*2 if input.kind is MULT
| |
| − | userSupport.applyTactic(BasicTactics.reasonerTac(
| |
| − | new ExampleReasoner(),
| |
| − | new ExampleReasoner.Input(hyp, position, kind)),
| |
| − | true, monitor);
| |
| − | } catch (RodinDBException e) {
| |
| − | // log the problem
| |
| − | }
| |
| − | }
| |
| − | }
| |
| | | | |
| − | // visits a formula and adds applications on occurrences of literal 4
| |
| − | private static class ExampleApplicationVisitor extends DefaultVisitor {
| |
| | | | |
| − | private final IUserSupport userSupport;
| |
| − | private final Predicate hyp;
| |
| − | private final Predicate predicate;
| |
| − | // a list to put applications into
| |
| − | private final List<ITacticApplication> applications;
| |
| | | | |
| − | public ExampleApplicationVisitor(IUserSupport userSupport,
| |
| − | Predicate predicate, Predicate hyp,
| |
| − | List<ITacticApplication> applications) {
| |
| − | this.userSupport = userSupport;
| |
| − | this.predicate = predicate;
| |
| − | this.hyp = hyp;
| |
| − | this.applications = applications;
| |
| − | }
| |
| | | | |
| − | @Override
| |
| − | public boolean visitINTLIT(IntegerLiteral lit) {
| |
| − | if (lit.getValue().intValue() == 4) {
| |
| − | final IPosition position = predicate.getPosition(lit.getSourceLocation());
| |
| − | applications.add(new ExampleApplication(userSupport, hyp, position, Kind.MULT));
| |
| − | applications.add(new ExampleApplication(userSupport, hyp, position, Kind.PLUS));
| |
| − | }
| |
| − | return true;
| |
| − | }
| |
| − | }
| |
| | | | |
| − | // the ITacticProvider2 interface method: calls the visitor on the predicate
| |
| − | public List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
| |
| − | IProofTreeNode node,
| |
| − | Predicate hyp,
| |
| − | String globalInput) {
| |
| | | | |
| − | final Predicate pred = (hyp == null) ? node.getSequent().goal() : hyp;
| |
| | | | |
| − | final List<ITacticApplication> applications = new ArrayList<ITacticApplication>();
| + | |
| − |
| + | {{TODO|Category}} |
| − | pred.accept(new ExampleApplicationVisitor(userSupport, pred, hyp, applications));
| |
| − |
| |
| − | return applications;
| |
| − | }
| |
| − | } | |
| − | </pre>
| |
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
This command is related to the "auto" or "manual" PO status. This status is visible in the explorer on each PO: it is marked with a 'A' at the upper right corner of the PO icon if it was entirely discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially).
Launching 'Recalculate Auto Status' reruns the current auto prover on selected POs. The main aim of this command is to update the "auto"/"manual" status to reflect the current auto prover configuration. In case a proof was previously automatically discharged and is no more, it will be marked as manually created.
This is intended to be used as a post-development operation to estimate the percentage of automated proofs over a changing auto prover. It is recommended to restore to the default auto provers before running this command.
Proof Replay on Undischarged POs
TODO
TODO: Category
