Rodin Proving Perspective: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r No edit summary |
||
| Line 8: | Line 8: | ||
== Loading a Proof == | == Loading a Proof == | ||
In order to load a proof, switch to the Proving Perspective, select the project from the Event-B Explorer, select and expand the component (context or machine), finally select the proof obligation of interest. The corresponding proof will be loaded. | In order to load a proof, switch to the Proving Perspective, select the project from the Event-B Explorer, select and expand the component (context or machine), finally select the proof obligation of interest. The corresponding proof will be loaded. | ||
== The Proof Tree == | |||
Revision as of 12:51, 11 March 2010
Overview
The Proving Perspective is made of a number of windows (views): the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Proof Information, and the Search Hypotheses. In subsequent sections, we study each of these windows. Below is a screenshot of the proving perspective:
Loading a Proof
In order to load a proof, switch to the Proving Perspective, select the project from the Event-B Explorer, select and expand the component (context or machine), finally select the proof obligation of interest. The corresponding proof will be loaded.
