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
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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