Difference between revisions of "Rodin Proving Perspective"
From Event-B
Jump to navigationJump to searchimported>Im06r |
imported>Im06r |
||
| 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
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.
