Difference between revisions of "Rodin Proving Perspective"
From Event-B
Jump to navigationJump to searchimported>Im06r |
imported>Im06r |
||
(4 intermediate revisions by the same user not shown) | |||
Line 3: | Line 3: | ||
== Overview == | == 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: | 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: | ||
+ | |||
+ | [[Image:ProvPers.png|center]] | ||
== Loading a Proof == | == Loading a Proof == | ||
− | In order to load 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. |
− | + | == The Proof Tree == | |
− | |||
− |
Revision as of 12:51, 11 March 2010
Contents |
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.