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

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.