Difference between revisions of "Rodin Proving Perspective"

From Event-B
Jump to navigationJump to search
imported>Im06r
imported>Im06r
Line 13: Line 13:
  
 
[[Image:ProTree.png|center]]
 
[[Image:ProTree.png|center]]
 +
 +
Each line in the tree corresponds to a node which is a sequent. A line is right shifted when the corresponding node is a direct descendant of the node of the previous line. Each node is labelled with a comment (description) explaining how it can be discharged. By selecting a node in the proof tree, the corresponding sequent is loaded: the hypotheses of the sequent are loaded to the Selected Hypotheses window, and the goal of the sequent is loaded to the Goal window.

Revision as of 13:42, 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:

ProTree.png

Each line in the tree corresponds to a node which is a sequent. A line is right shifted when the corresponding node is a direct descendant of the node of the previous line. Each node is labelled with a comment (description) explaining how it can be discharged. By selecting a node in the proof tree, the corresponding sequent is loaded: the hypotheses of the sequent are loaded to the Selected Hypotheses window, and the goal of the sequent is loaded to the Goal window.