Proof Obligation Commands
From Event-B
Revision as of 16:42, 4 March 2010 by imported>Nicolas (New page: In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: Image:PO_Commands.png These commands are run on all POs located un...)
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
TODO
Recalculate Auto Status
TODO
Proof Replay on Undischarged POs
TODO
TODO: Category
