Rodin Proving Perspective: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r |
||
| Line 11: | Line 11: | ||
== The Proof Tree == | == The Proof Tree == | ||
The proof tree describe each individual proof step in the proof. The proof tree can be seen in its corresponding window as seen in the following screenshot: | The proof tree describe each individual proof step in the proof. The proof tree can be seen in its corresponding window as seen in the following screenshot: | ||
[[Image:ProTree.png|center]] | |||
Revision as of 13:16, 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.
The Proof Tree
The proof tree describe each individual proof step in the proof. The proof tree can be seen in its corresponding window as seen in the following screenshot:
