Difference between pages "Proof Skeleton Design" and "Proof Skeleton View"
imported>Nicolas (New page: This document aims at helping developers getting into the code of the proof skeleton viewer. ==Purpose== The Proof Skeleton View gives the user the ability to quickly browse the skeleton...) |
imported>Mathieu |
||
| Line 1: | Line 1: | ||
| − | |||
| − | |||
==Purpose== | ==Purpose== | ||
The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a convenient way to display rules and sequents together in the same view. | The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a convenient way to display rules and sequents together in the same view. | ||
| − | == | + | ==The Proof Skeleton View== |
| + | |||
| + | ===Showing the View=== | ||
| + | |||
| + | The Proof Skeleton View is available as other views in the | ||
| + | Window > Show View > Other > Event-B > Proof Skeleton View | ||
| + | menu. | ||
| + | |||
| + | To watch a proof skeleton, simply select a proved predicate in the obligation explorer, or a proof file in the editor. | ||
| − | + | ===View Interpretation=== | |
| − | + | Proof skeletons are displayed in a two-part view. On the left hand side is the tree structure of rules applied in the proof. On the other side stands the sequent on which the currently selected rule is applied. | |
| − | |||
| − | + | [[Image:proofSkeletonView.jpg]] | |
| − | The | + | The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner. |
| − | |||
| − | + | [[Category:User Documentation]] | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Revision as of 13:08, 12 December 2008
Purpose
The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a convenient way to display rules and sequents together in the same view.
The Proof Skeleton View
Showing the View
The Proof Skeleton View is available as other views in the Window > Show View > Other > Event-B > Proof Skeleton View menu.
To watch a proof skeleton, simply select a proved predicate in the obligation explorer, or a proof file in the editor.
View Interpretation
Proof skeletons are displayed in a two-part view. On the left hand side is the tree structure of rules applied in the proof. On the other side stands the sequent on which the currently selected rule is applied.
The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner.
