Difference between revisions of "Rodin Proving Perspective"
From Event-B
Jump to navigationJump to searchimported>Im06r |
imported>Im06r |
||
Line 7: | Line 7: | ||
== 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, 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. |
Revision as of 12:49, 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.