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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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

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