Difference between pages "Extension Proof Rules" and "File:Steve Wright Quite Big Model Presentation.pdf"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m
 
 
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
Slides from Steve Wright's presentation "Experiences with a Quite Big Event-b Model", given at the Rodin workshop, Southampton, July 16th 2009.
Rules without a <tt>*</tt> are planned to be implemented in future versions.
 
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 
 
 
== Rewrite Rules ==
 
 
 
{{RRHeader}}
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math>  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math>  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 </math>||  ||  A
 
|}
 
 
 
 
 
== Inference Rules ==
 
{{RRHeader}}
 
 
 
|}
 
 
 
[[Category:User documentation|The Proving Perspective]]
 
[[Category:Rodin Platform|The Proving Perspective]]
 
[[Category:User manual|The Proving Perspective]]
 

Latest revision as of 20:49, 30 April 2020

Slides from Steve Wright's presentation "Experiences with a Quite Big Event-b Model", given at the Rodin workshop, Southampton, July 16th 2009.