Rodin Proving Perspective

From Event-B
Revision as of 12:49, 11 March 2010 by imported>Im06r (→‎Loading a Proof)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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, finally select the proof obligation of interest. The corresponding proof will be loaded.