Difference between pages "Rodin Proving Perspective" and "CamilleX"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
 
Line 1: Line 1:
−
{{Navigation|Previous= [[The_Proof_Obligation_Explorer_(Rodin_User_Manual)|The Proof Obligation Explorer]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}}
 
 
{{TOCright}}
 
{{TOCright}}
−
== Overview ==
+
Return to [[Rodin Plug-ins]]
−
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:
 
−
[[Image:ProvPers.png|center]]
 
  
−
== Loading a Proof ==
+
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
−
In order to load a proof, enter the Proof Obligation window, select the project, select and expand the component, finally select the proof obligation: the corresponding proof will be loaded. As a consequence:
+
Extension to Event-B including the ''machine inclusion'' mechanism is also supported.
  
−
* the proof tree is loaded in the Proof Tree window. As we shall see in section [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Tree|6.2]], each node of the proof tree is associated with a sequent.
+
<br style="clear: both" />
−
* In case the proof tree has some "pending" nodes (whose sequents are not discharged yet) then the sequent corresponding to the first pending node is decomposed: its goal is loaded in the Goal window (section [[The_Proving_Perspective_(Rodin_User_Manual)#Goal and Selected Hypotheses|6.3]]), whereas parts of its hypotheses (the "selected" ones) are loaded in the Selected Hypotheses window (section [[The_Proving_Perspective_(Rodin_User_Manual)#Goal and Selected Hypotheses|6.3]]).
+
 
−
* In case the proof tree has no pending node, then the sequent of the root node is loaded as explained previously.
+
Please have a look also at the [[CamilleX User Guide]].
 +
 
 +
=== Current version ===
 +
The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the ''CamilleX'' category).  Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.
 +
 
 +
=== Principles ===
 +
The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.

Latest revision as of 13:09, 19 July 2021

Return to Rodin Plug-ins

The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. Extension to Event-B including the machine inclusion mechanism is also supported.


Please have a look also at the CamilleX User Guide.

Current version

The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the CamilleX category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.

Principles

The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Proving_Perspective&oldid=14477’