Difference between revisions of "Rodin Proving Perspective"

From Event-B
Jump to navigationJump to search
imported>Im06r
imported>Im06r
Line 10: Line 10:
  
 
== 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:

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:

ProvPers.png

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: