Difference between pages "Relation Rewrite Rules" and "Rodin Workshop 2014"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m (added DERIV_DOM_TOTALREL)
 
imported>Stefan
 
Line 1: Line 1:
−
{{RRHeader}}
+
==5th Rodin User and Developer Workshop==
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_COMPSET}}||<math>  \dom (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ x, \ldots , y\} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_CONVERSE}}||<math>  \dom (r^{-1} ) \;\;\defi\;\;  \ran (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_COMPSET}}||<math>  \ran (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ a, \ldots , b\} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_CONVERSE}}||<math>  \ran (r^{-1} ) \;\;\defi\;\;  \dom (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OVERL}}||<math>  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OVERL}}||<math>\begin{array}{cl} & r \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \\ \defi &  r \ovl  \ldots  \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \end{array}</math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_OVERL_CPROD}}||<math>  r \ovl  (\mathit{Ty} \cprod  S) \;\;\defi\;\;  (\mathit{Ty} \cprod  S) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_L}}||<math>  \emptyset  \domres  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_R}}||<math>  S \domres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOMRES}}||<math> \mathit{Ty} \domres  r \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMRES_DOM}}||<math>  \dom (r) \domres  r \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMRES_RAN}}||<math>  \ran (r) \domres  r^{-1}  \;\;\defi\;\;  r^{-1} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOMRES_ID}}||<math>  S \domres  \id (T) \;\;\defi\;\;  \id (S \binter  T) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_R}}||<math>  r \ranres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_L}}||<math>  \emptyset  \ranres  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RANRES}}||<math>  r \ranres  \mathit{Ty} \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_RAN}}||<math>  r \ranres  \ran (r) \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_DOM}}||<math>  r^{-1}  \ranres  \dom (r) \;\;\defi\;\;  r^{-1} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RANRES_ID}}||<math>  \id (S) \ranres  T \;\;\defi\;\;  \id (S \binter  T) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_L}}||<math>  \emptyset  \domsub  r \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_R}}||<math>  S \domsub  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOMSUB}}||<math> \mathit{Ty} \domsub  r \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMSUB_DOM}}||<math>  \dom (r) \domsub  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOMSUB_ID}}||<math>  S \domsub  \id (T) \;\;\defi\;\;  \id (T \setminus S) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_R}}||<math>  r \ransub  \emptyset  \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_L}}||<math>  \emptyset  \ransub  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RANSUB}}||<math>  r \ransub  \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANSUB_RAN}}||<math>  r \ransub  \ran (r) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RANSUB_ID}}||<math>  \id (S) \ransub  T \;\;\defi\;\;  \id (S \setminus T) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_FCOMP}}||<math>  r \fcomp \ldots  \fcomp \emptyset  \fcomp \ldots  \fcomp s \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_FCOMP_ID}}||<math>  r \fcomp \ldots  \fcomp \id (\mathit{Ty}) \fcomp \ldots  \fcomp s \;\;\defi\;\;  r \fcomp \ldots  \fcomp s </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_FCOMP_R}}||<math>  r \fcomp \mathit{Ty} \;\;\defi\;\;  \dom (r) \cprod  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_FCOMP_L}}||<math> \mathit{Ty} \fcomp r \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID}}||<math>  r \fcomp \ldots  \fcomp \id (S) \fcomp \id (T) \fcomp \ldots  s \;\;\defi\;\;  r \fcomp \ldots  \fcomp \id (S \binter  T) \fcomp \ldots  \fcomp s </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  \emptyset  \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BCOMP_ID}}||<math>  r \bcomp  \ldots  \bcomp  \id (\mathit{Ty}) \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp  s </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BCOMP_L}}||<math> \mathit{Ty} \bcomp  r \;\;\defi\;\;  \dom (r) \cprod  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BCOMP_R}}||<math>  r \bcomp  \mathit{Ty} \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_BCOMP_ID}}||<math>  r \bcomp  \ldots  \bcomp  \id (S) \bcomp  \id (T) \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp  \id (S \binter  T) \bcomp  \ldots  \bcomp  s </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_R}}||<math>  r \dprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_L}}||<math>  \emptyset  \dprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DPROD}}||<math> \mathit{Ta} \dprod  \mathit{Tb} \;\;\defi\;\;  Tc \cprod  (Td \cprod  Te) </math>|| where <math>\mathit{Ta}</math> and <math>\mathit{Tb}</math> are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Tc} \cprod \mathit{Te}</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_R}}||<math>  r \pprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_L}}||<math>  \emptyset  \pprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_PPROD}}||<math> \mathit{Ta} \pprod  \mathit{Tb} \;\;\defi\;\;  (Tc \cprod  Te) \cprod  (Td \cprod  Tf) </math>|| where <math>\mathit{Ta}</math> and <math>\mathit{Tb}</math> are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Te} \cprod \mathit{Tf}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RELIMAGE_R}}||<math>  r[\emptyset ] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RELIMAGE_L}}||<math>  \emptyset [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RELIMAGE}}||<math>  r[Ty] \;\;\defi\;\;  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_DOM}}||<math>  r[\dom (r)] \;\;\defi\;\;  \ran (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RELIMAGE_ID}}||<math>  \id (\mathit{Ty})[T] \;\;\defi\;\;  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_ID}}||<math>  \id (S)[T] \;\;\defi\;\;  S \binter  T </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CPROD_SING}}||<math>  (\{ E\}  \cprod  S)[\{ E\} ] \;\;\defi\;\;  S </math>|| where <math>E</math> is a single expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_SING_MAPSTO}}||<math>  \{ E \mapsto  F\} [\{ E\} ] \;\;\defi\;\;  \{ F\} </math>|| where <math>E</math> is a single expression ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB}}||<math>  (r \ransub  S)^{-1} [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANRES}}||<math>  (r \ranres  S)^{-1} [S] \;\;\defi\;\;  r^{-1} [S] </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_CONVERSE_DOMSUB}}||<math>  (S \domsub  r)^{-1} [T] \;\;\defi\;\;  r^{-1} [T] \setminus S </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_RANSUB}}||<math>  (r \ransub  S)[T] \;\;\defi\;\;  r[T] \setminus S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_RANRES}}||<math>  (r \ranres  S)[T] \;\;\defi\;\;  r[T] \binter  S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[T] \;\;\defi\;\;  r[T \setminus S] </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_DOMRES}}||<math>  (S \domres  r)[T] \;\;\defi\;\;  r[S \binter  T] </math>||  ||  M
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CONVERSE}}||<math>  \emptyset ^{-1}  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_ID}}||<math>  \id (S)^{-1}  \;\;\defi\;\;  \id (S) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_CONVERSE}}||<math> \mathit{Ty}^{-1}  \;\;\defi\;\;  \mathit{Tb} \cprod  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_SETENUM}}||<math>  \{ x \mapsto  a, \ldots , y \mapsto  b\} ^{-1}  \;\;\defi\;\;  \{ a \mapsto  x, \ldots , b \mapsto  y\} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_COMPSET}}||<math>  \{ x, \ldots , y \qdot  P \mid  x, \ldots , y\} ^{-1}  \;\;\defi\;\;  \{ y, \ldots , x \qdot  P \mid  y, \ldots , x\} </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_ID}}||<math>  \id (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_ID}}||<math>  \dom (\id (S)) \;\;\defi\;\;  S </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_ID}}||<math>  \ran (\id (S)) \;\;\defi\;\;  S </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_L}}||<math>  (\id (S) \fcomp r) \;\;\defi\;\;  S \domres  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_R}}||<math>  r \fcomp \id (S) \;\;\defi\;\;  r \ranres  S </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_R}}||<math>  S \rel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\srel  \pfun  \pinj  \psur</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_L}}||<math>  \emptyset  \rel  S \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\trel  \pfun  \tfun  \pinj  \tinj</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math>  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse </math>|| idem for operators <math>\pfun  \pinj</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math>  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset </math>|| idem for operators <math>\tfun  \tinj  \tsur  \tbij</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PRJ1}}||<math>  \prjone (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PRJ2}}||<math>  \prjtwo (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ1}}||<math>  \prjone (r)(E \mapsto  F) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ2}}||<math>  \prjtwo (r)(E \mapsto  F) \;\;\defi\;\;  F </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_PRJ1}}||<math>  \dom (\prjone (r)) \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_PRJ2}}||<math>  \dom (\prjtwo (r)) \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_PRJ1}}||<math>  \ran (\prjone (r)) \;\;\defi\;\;  \dom (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_PRJ2}}||<math>  \ran (\prjtwo (r)) \;\;\defi\;\;  \ran (r) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_LAMBDA}}||<math>  (\lambda x \qdot  \bfalse  \mid  E) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_LAMBDA}}||<math>  (\lambda x \qdot  P(x) \mid  E(x))(y) \;\;\defi\;\;  E(y) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_LAMBDA}}||<math>  \dom (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  x\} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_LAMBDA}}||<math>  \ran (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  E\} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LL}}||<math>  \{ A \mapsto  E, \ldots  , B \mapsto  E\} (x) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LR}}||<math>  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} (x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_OVERL_SETENUM}}||<math>  (r \ovl  \ldots  \ovl  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_BUNION_SETENUM}}||<math>  (r \bunion  \ldots  \bunion  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CPROD}}||<math>  (S \cprod  \{ F\} )(x) \;\;\defi\;\;  F </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_ID}}||<math>  \id (S)(x) \;\;\defi\;\;  x </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE}}||<math>  f(f^{-1} (E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CONVERSE_FUNIMAGE}}||<math>  f^{-1}(f(E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM}}||<math>  \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DEF_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  s \fcomp \ldots  \fcomp r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_ID_SING}}||<math>  \id (\{ E\} ) \;\;\defi\;\;  \{ E \mapsto  E\} </math>|| where <math>E</math> is a single expression ||  M
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOM}}||<math>  \dom (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RAN}}||<math>  \ran (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_CONVERSE}}||<math>  r^{-1-1}  \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_FCOMP}}||<math>  (p \fcomp q)[s] \;\;\defi\;\;  q[p[s]] </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMRES}}||<math>  (s \domres  p) \fcomp q \;\;\defi\;\;  s \domres  (p \fcomp q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMSUB}}||<math>  (s \domsub  p) \fcomp q \;\;\defi\;\;  s \domsub  (p \fcomp q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANRES}}||<math>  p \fcomp (q \ranres  s) \;\;\defi\;\;  (p \fcomp q) \ranres  s </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANSUB}}||<math>  p \fcomp (q \ransub  s) \;\;\defi\;\;  (p \fcomp q) \ransub  s </math>||  ||  M
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOMRAN}}||<math>  \emptyset  \strel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\tsur  \tbij</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOM}}||<math>  \dom (\mathit{Ty}) \;\;\defi\;\;  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RAN}}||<math>  \ran (\mathit{Ty}) \;\;\defi\;\;  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_CPROD}}||<math>  \dom (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_CPROD}}||<math>  \ran (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOM}}||<math>  E \in  \dom (r) \;\;\defi\;\;  \exists y \qdot  E \mapsto  y \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RAN}}||<math>  F \in  \ran (r) \;\;\defi\;\;  \exists x \qdot  x \mapsto  F  \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_CONVERSE}}||<math>  E \mapsto  F \in  r^{-1}  \;\;\defi\;\;  F \mapsto  E \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOMRES}}||<math>  E \mapsto  F \in  S \domres  r \;\;\defi\;\;  E \in  S \land  E \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RANRES}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \in  T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOMSUB}}||<math>  E \mapsto  F \in  S \domsub  r \;\;\defi\;\;  E \notin  S \land  E \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RANSUB}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \notin  T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELIMAGE}}||<math>  F \in  r[w] \;\;\defi\;\;  \exists x \qdot  x \in  w \land  x \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_FCOMP}}||<math>  E \mapsto  F \in  (p \fcomp q) \;\;\defi\;\;  \exists x \qdot  E \mapsto  x \in  p \land  x \mapsto  F \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_OVERL}}||<math>  p \ovl  q \;\;\defi\;\;  (\dom (q) \domsub  p) \bunion  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_ID}}||<math>  E \mapsto  F \in  \id (S) \;\;\defi\;\;  E \in  S \land  F = E </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DPROD}}||<math>  E \mapsto  (F \mapsto  G) \in  p \dprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  E \mapsto  G \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_PPROD}}||<math>  (E \mapsto  G) \mapsto  (F \mapsto  H) \in  p \pprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  G \mapsto  H \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOM}}||<math>  r \in  S \trel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELRAN}}||<math>  r \in  S \trel  T \;\;\defi\;\;  r \in  S \rel  T \land  \ran (r) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOMRAN}}||<math>  r \in  S \strel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S \land  \ran (r) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_FCT}}||<math>\begin{array}{rcl}
 
−
f \in  S \pfun  T & \defi & f \in  S \rel  T  \\  & \land & (\forall x,y,z \qdot  x \mapsto  y \in  f \land  x \mapsto  z \in  f \limp  y = z) \\ \end{array} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_TFCT}}||<math>  f \in  S \tfun  T \;\;\defi\;\;  f \in  S \pfun  T \land  \dom (f) = S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_INJ}}||<math>  f \in  S \pinj  T \;\;\defi\;\;  f \in  S \pfun  T \land  f^{-1}  \in  T \pfun  S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_TINJ}}||<math>  f \in  S \tinj  T \;\;\defi\;\;  f \in  S \pinj  T \land  \dom (f) = S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_SURJ}}||<math>  f \in  S \pfun  T \;\;\defi\;\;  f \in  S \pfun  T \land  \ran (f) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_TSURJ}}||<math>  f \in  S \tsur  T \;\;\defi\;\;  f \in  S \psur  T \land  \dom (f) = S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_BIJ}}||<math>  f \in  S \tbij  T \;\;\defi\;\;  f \in  S \tinj  T \land  \ran (f) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_BCOMP_BUNION}}||<math>  r \bcomp  (s \bunion  t) \;\;\defi\;\;  (r \bcomp  s) \bunion  (r \bcomp  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_FCOMP_BUNION_R}}||<math>  p \fcomp (q \bunion  r) \;\;\defi\;\;  (p \fcomp q) \bunion  (p \fcomp r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_FCOMP_BUNION_L}}||<math>  (q \bunion  r) \fcomp p \;\;\defi\;\;  (q \fcomp p) \bunion  (r \fcomp p) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_BUNION}}||<math>  r \dprod  (s \bunion  t) \;\;\defi\;\;  (r \dprod  s) \bunion  (r \dprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_BINTER}}||<math>  r \dprod  (s \binter  t) \;\;\defi\;\;  (r \dprod  s) \binter  (r \dprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_SETMINUS}}||<math>  r \dprod  (s \setminus t) \;\;\defi\;\;  (r \dprod  s) \setminus (r \dprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_OVERL}}||<math>  r \dprod  (s \ovl  t) \;\;\defi\;\;  (r \dprod  s) \ovl  (r \dprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_BUNION}}||<math>  r \pprod  (s \bunion  t) \;\;\defi\;\;  (r \pprod  s) \bunion  (r \pprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_BINTER}}||<math>  r \pprod  (s \binter  t) \;\;\defi\;\;  (r \pprod  s) \binter  (r \pprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_SETMINUS}}||<math>  r \pprod  (s \setminus t) \;\;\defi\;\;  (r \pprod  s) \setminus (r \pprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_OVERL}}||<math>  r \pprod  (s \ovl  t) \;\;\defi\;\;  (r \pprod  s) \ovl  (r \pprod  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_OVERL_BUNION_L}}||<math>  (p \bunion  q) \ovl  r \;\;\defi\;\;  (p \ovl  r) \bunion  (q \ovl  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_OVERL_BINTER_L}}||<math>  (p \binter  q) \ovl  r \;\;\defi\;\;  (p \ovl  r) \binter  (q \ovl  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BUNION_R}}||<math>  s \domres  (p \bunion  q) \;\;\defi\;\;  (s \domres  p) \bunion  (s \domres  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BUNION_L}}||<math>  (s \bunion  t) \domres  r \;\;\defi\;\;  (s \domres  r) \bunion  (t \domres  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BINTER_R}}||<math>  s \domres  (p \binter  q) \;\;\defi\;\;  (s \domres  p) \binter  (s \domres  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BINTER_L}}||<math>  (s \binter  t) \domres  r \;\;\defi\;\;  (s \domres  r) \binter  (t \domres  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_SETMINUS_R}}||<math>  s \domres  (p \setminus q) \;\;\defi\;\;  (s \domres  p) \setminus (s \domres  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_SETMINUS_L}}||<math>  (s \setminus t) \domres  r \;\;\defi\;\;  (s \domres  r) \setminus (t \domres  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_DPROD}}||<math>  s \domres  (p \dprod  q) \;\;\defi\;\;  (s \domres  p) \dprod  (s \domres  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_OVERL}}||<math>  s \domres  (r \ovl  q) \;\;\defi\;\;  (s \domres  r) \ovl  (s \domres  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_R}}||<math>  s \domsub  (p \bunion  q) \;\;\defi\;\;  (s \domsub  p) \bunion  (s \domsub  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_L}}||<math>  (s \bunion  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \bunion  (t \domsub  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_R}}||<math>  s \domsub  (p \binter  q) \;\;\defi\;\;  (s \domsub  p) \binter  (s \domsub  q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_L}}||<math>  (s \binter  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \binter  (t \domsub  r) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_DPROD}}||<math>  A \domsub  (r \dprod  s) \;\;\defi\;\;  (A \domsub  r) \dprod  (A \domsub  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_OVERL}}||<math>  A \domsub  (r \ovl  s) \;\;\defi\;\;  (A \domsub  r) \ovl  (A \domsub  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BUNION_R}}||<math>  r \ranres (s \bunion t) \;\;\defi\;\;  (r \ranres  s) \bunion  (r \ranres  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BUNION_L}}||<math>  (p \bunion  q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \bunion  (q \ranres  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BINTER_R}}||<math>  r \ranres (s \binter t) \;\;\defi\;\;  (r \ranres  s) \binter  (r \ranres  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BINTER_L}}||<math>  (p \binter  q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \binter  (q \ranres  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_R}}||<math>  r \ranres  (s \setminus t) \;\;\defi\;\;  (r \ranres  s) \setminus (r \ranres  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<math>  (p \setminus q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \setminus (q \ranres  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_R}}||<math>  (r \bunion  s) \ransub  t \;\;\defi\;\;  (r \ransub  t) \bunion  (s \ransub  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<math>  (p \bunion  q) \ransub  s \;\;\defi\;\;  (p \ransub  s) \bunion  (q \ransub  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_R}}||<math>  (r \binter  s) \ransub  t \;\;\defi\;\;  (r \ransub  t) \binter  (s \ransub  t) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<math>  (p \binter  q) \ransub  s \;\;\defi\;\;  (p \ransub  s) \binter  (q \ransub  s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BUNION}}||<math>  (p \bunion  q)^{-1}  \;\;\defi\;\;  p^{-1}  \bunion  q^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BINTER}}||<math>  (p \binter  q)^{-1}  \;\;\defi\;\;  p^{-1}  \binter  q^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_SETMINUS}}||<math>  (r \setminus s)^{-1}  \;\;\defi\;\;  r^{-1}  \setminus s^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BCOMP}}||<math>  (r \bcomp  s)^{-1}  \;\;\defi\;\;  (s^{-1}  \bcomp  r^{-1} ) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_FCOMP}}||<math>  (p \fcomp q)^{-1}  \;\;\defi\;\;  (q^{-1}  \fcomp p^{-1} ) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_PPROD}}||<math>  (r \pprod  s)^{-1}  \;\;\defi\;\;  r^{-1}  \pprod  s^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_DOMRES}}||<math>  (s \domres  r)^{-1}  \;\;\defi\;\;  r^{-1}  \ranres  s </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_DOMSUB}}||<math>  (s \domsub  r)^{-1}  \;\;\defi\;\;  r^{-1}  \ransub  s </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_RANRES}}||<math>  (r \ranres  s)^{-1}  \;\;\defi\;\;  s \domres  r^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_RANSUB}}||<math>  (r \ransub  s)^{-1}  \;\;\defi\;\;  s \domsub  r^{-1} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOM_BUNION}}||<math>  \dom (r \bunion  s) \;\;\defi\;\;  \dom (r) \bunion  \dom (s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<math>  \ran (r \bunion  s) \;\;\defi\;\;  \ran (r) \bunion  \ran (s) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_R}}||<math>  r[S \bunion  T] \;\;\defi\;\;  r[S] \bunion  r[T] </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_L}}||<math>  (p \bunion  q)[S] \;\;\defi\;\;  p[S] \bunion  q[S] </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_DOM_BUNION}}||<math>  \dom (p \bunion  q) \;\;\defi\;\;  \dom (p) \bunion  \dom (q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<math>  \ran (p \bunion  q) \;\;\defi\;\;  \ran (p) \bunion  \ran (q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_DOM_TOTALREL}}||<math>  \dom (r) \;\;\defi\;\;  E </math> || with hypothesis <math>r \in E \mathit{op} F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> ||  M
 
  
 +
''June 2-3, 2014''
 +
 +
Toulouse
 +
 +
http://wiki.event-b.org/index.php/Rodin_Workshop_2014
 +
 +
The purpose of the Rodin workshop
 +
is to bring together existing and potential users and developers of the Rodin
 +
toolset and to foster a broader community of Rodin users and developers.
 +
For Rodin users the workshop will provide an opportunity to share tool
 +
experiences and to gain an understanding of on-going tool developments.
 +
For plug-in developers the workshop will provide an opportunity to
 +
showcase their tools and to achieve better coordination of tool
 +
development effort.
 +
 +
Previous Rodin User and Developer Workshops were held at Abo Akademi, the University of
 +
Southampton, the University of Düsseldorf and the University of Paris-Est Créteil.
 +
 +
The 5th Rodin workshop will be collocated with the [http://www.irit.fr/ABZ2014/ ABZ 2014 conference].
 +
 +
The format will be presentations together with plenty of time for discussion.
 +
On day 1 in the morning a Demonstrator and Developer Tutorial will be held
 +
while the remaining 1.5 days will be devoted to tool usage and tool developments.
 +
 +
If you are interested in giving a presentation at the Rodin workshop or
 +
have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF)
 +
to rodin@ecs.soton.ac.uk by:
 +
*        14 April 2014.
 +
 +
Indicate whether it is a tool usage or tool development presentation.
 +
Plug-in presentations may be about existing developments or planned
 +
future developments. We will endeavour to accommodate all submissions
 +
that are clearly relevant to Rodin and Event-B.
 +
 +
== Programme ==
 +
 +
<b>Monday 2 June 2014</b>
 +
{|
 +
| 08h45 - 09h00 || <b>REGISTRATION</b>
 +
|-
 +
| 09h00 - 10h30 || Practical Theory Extension Tutorial session 1
 +
|-
 +
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
 +
|-
 +
| 10h30 - 11h00 || <b>BREAK</b>
 +
|-
 +
| 11h00 - 12h30 || Practical Theory Extension Tutorial session 2
 +
|-
 +
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
 +
|}
 +
{|
 +
|-
 +
| 12h30 - 14h00 || <b>LUNCH</b>
 +
|-
 +
| 14h00 - 15h20 || <b>Tool use</b>
 +
|-
 +
| || 14h00 || Modeling a Safe Interlocking Using the Event-B Theory Plug-in
 +
|-
 +
| || || Thang Khuu, Laurent Voisin, Fernando Mejia
 +
|-
 +
| || 14h20 || Unlocking the Mysteries of a Formal Model of an Interlocking System
 +
|-
 +
| || || Michael Leuschel, Jens Bendisposto and Dominik Hansen
 +
|-
 +
| || 14h40 || Run-time Management of Many-core Systems using Rodin
 +
|-
 +
| || || Asieh Salehi, Colin Snook, Michael Butler
 +
|-
 +
| || 15h00 || An Experiment in Modeling Satellite Flight Formation in Event-B
 +
|-
 +
| || || Inna Pereverzeva, Anton Tarasyuk, Elena Troubitsyna
 +
|-
 +
| 15h20 - 16h00 || <b>BREAK</b>
 +
|-
 +
| 16h00 - 17h20 || <b>Tool use</b>
 +
|-
 +
| || 16h00 || Developing and Proving a Complicated System Model with Rodin
 +
|-
 +
| || || A. V. Khoroshilov, I. V. Shchepetkov
 +
|-
 +
| || 16h20 || Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns
 +
|-
 +
| || || Zeineb Graja, Frederic Migeon, Christine Maurel, Marie-Pierre Gleizes, Ahmed Hadj Kacem
 +
|-
 +
| || 16h40 || Generating Tests for COTS Components with Event-B and STPA
 +
|-
 +
| || || Toby Wilkinson, Michael Butler, John Colley, Colin Snook
 +
|-
 +
| || 17h00 || Towards Verified Implementation of Event-B Models in Dafny
 +
|-
 +
| || || Mohammadsadegh Dalvandi, Michael Butler
 +
|-
 +
| 17h20 - 18h00 || <b>Tool development</b>
 +
|-
 +
| || 17h20 || Code Generation – Tool Developments
 +
|-
 +
| || || Andy Edmunds
 +
|-
 +
| || 17h40 || Toolbox for penetration testing based on Rodin and ProB
 +
|-
 +
| || || Aymerick Savary, Marc Frappier, Jean-Louis Lanet
 +
|}
 +
<b>Tuesday 3 June 2014</b>
 +
{|
 +
| 09h00 - 10h20 || <b>Tool development</b>
 +
|-
 +
| || 09h00 || iUML-B Statemachines
 +
|-
 +
| || || Colin Snook
 +
|-
 +
| || 09h20 || EB2RC: A Rodin plug-in for visualising Event-B models and code generation
 +
|-
 +
| || || Zheng Cheng, Dominique Mery, Rosemary Monahan
 +
|-
 +
| || 09h40 || Composition Operators for Event-B. CO4EB Rodin plugin
 +
|-
 +
| || || Idir Ait-Sadoune, Yamine Ait- Ameur
 +
|-
 +
| || 10h00 || CODA Update: New Features for 2014
 +
|-
 +
| || || Neil Evans, Helen Marshall, James Sharp, Michael Butler, John Colley, Colin Snook
 +
|-
 +
| 10h20 - 11h00 || <b>BREAK</b>
 +
|-
 +
| 11h00 - 11h40 || <b>Tool development</b>
 +
|-
 +
| || 11h00 || A Practical Approach for Validation with Rodin Theories
 +
|-
 +
| || || Daniel Plagge, Michael Leuschel
 +
|-
 +
| || 11h20 || Rodin Multi-Simulation Plug-in
 +
|-
 +
| || || Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto
 +
|-
 +
| 11h40 - 12h00 || <b>Teaching</b>
 +
|-
 +
| || 11h40 || Formal Methods, Requirements and Software Engineering
 +
|-
 +
| || || Ken Robinson
 +
|-
 +
| 12h00 - 12h20 || <b>Theory</b>
 +
|-
 +
| || 12h00 || Responsiveness and Event-B
 +
|-
 +
| || || James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook
 +
|-
 +
| 12h20 - 14h00 || <b>LUNCH</b>
 +
|-
 +
| 14h00 - 15h20 || <b>Theory</b>
 +
|-
 +
| || 14h00 || Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events)
 +
|-
 +
| || || Jean-Raymond Abrial
 +
|-
 +
| || 14h20 || Program Development in Event-B with Proof Outlines
 +
|-
 +
| || || Stefan Hallerstede
 +
|-
 +
| || 14h40 || Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
 +
|-
 +
| || || Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi
 +
|-
 +
| || 15h00 || Smart Grids: Multi-Simulation, An Application
 +
|-
 +
| || || Brett Bicknell, Karim Kanso, Jose Reis
 +
|-
 +
| 15h20 - 16h00 || <b>BREAK</b>
 +
|-
 +
| 16h00 - 17h40 || <b>Theory</b>
 +
|-
 +
| || 16h00 || Towards Patterns for Statemachine Modelling under Timing Constraints
 +
|-
 +
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh
 +
|-
 +
| || 16h20 || From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B
 +
|-
 +
| || || John Colley, Michael Butler
 +
|-
 +
| || 16h40 || Event-B for Safety Analysis of Critical Systems
 +
|-
 +
| || || Matthias Gudemann and Marielle Petit-Doche
 +
|-
 +
| || 17h00 || Modelling Of Systems Of Systems - An Event-B Perspective Of a VDM Project
 +
|-
 +
| || || Stefan Hallerstede , Klaus Kristensen, Peter Gorm Larsen
 
|}
 
|}
  
 +
==Organisers==
 +
 +
Michael Butler, University of Southampton
 +
 +
Stefan  Hallerstede, Aarhus University
 +
 +
Thierry Lecomte, ClearSy
 +
 +
Michael Leuschel, University of Düsseldorf
 +
 +
Alexander Romanovsky, Newcastle University
  
 +
Laurent Voisin, Systerel
  
−
[[Category:User documentation|The Proving Perspective]]
+
Marina Walden, Åbo Akademi University
−
[[Category:Rodin Platform|The Proving Perspective]]
 
−
[[Category:User manual|The Proving Perspective]]
 

Revision as of 16:01, 29 April 2014

5th Rodin User and Developer Workshop

June 2-3, 2014

Toulouse

http://wiki.event-b.org/index.php/Rodin_Workshop_2014

The purpose of the Rodin workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.

Previous Rodin User and Developer Workshops were held at Abo Akademi, the University of Southampton, the University of Düsseldorf and the University of Paris-Est Créteil.

The 5th Rodin workshop will be collocated with the ABZ 2014 conference.

The format will be presentations together with plenty of time for discussion. On day 1 in the morning a Demonstrator and Developer Tutorial will be held while the remaining 1.5 days will be devoted to tool usage and tool developments.

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to rodin@ecs.soton.ac.uk by:

  • 14 April 2014.

Indicate whether it is a tool usage or tool development presentation. Plug-in presentations may be about existing developments or planned future developments. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

Programme

Monday 2 June 2014

08h45 - 09h00 REGISTRATION
09h00 - 10h30 Practical Theory Extension Tutorial session 1
Asieh Salehi, Jean-Raymond Abrial, Michael Butler
10h30 - 11h00 BREAK
11h00 - 12h30 Practical Theory Extension Tutorial session 2
Asieh Salehi, Jean-Raymond Abrial, Michael Butler
12h30 - 14h00 LUNCH
14h00 - 15h20 Tool use
14h00 Modeling a Safe Interlocking Using the Event-B Theory Plug-in
Thang Khuu, Laurent Voisin, Fernando Mejia
14h20 Unlocking the Mysteries of a Formal Model of an Interlocking System
Michael Leuschel, Jens Bendisposto and Dominik Hansen
14h40 Run-time Management of Many-core Systems using Rodin
Asieh Salehi, Colin Snook, Michael Butler
15h00 An Experiment in Modeling Satellite Flight Formation in Event-B
Inna Pereverzeva, Anton Tarasyuk, Elena Troubitsyna
15h20 - 16h00 BREAK
16h00 - 17h20 Tool use
16h00 Developing and Proving a Complicated System Model with Rodin
A. V. Khoroshilov, I. V. Shchepetkov
16h20 Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns
Zeineb Graja, Frederic Migeon, Christine Maurel, Marie-Pierre Gleizes, Ahmed Hadj Kacem
16h40 Generating Tests for COTS Components with Event-B and STPA
Toby Wilkinson, Michael Butler, John Colley, Colin Snook
17h00 Towards Verified Implementation of Event-B Models in Dafny
Mohammadsadegh Dalvandi, Michael Butler
17h20 - 18h00 Tool development
17h20 Code Generation – Tool Developments
Andy Edmunds
17h40 Toolbox for penetration testing based on Rodin and ProB
Aymerick Savary, Marc Frappier, Jean-Louis Lanet

Tuesday 3 June 2014

09h00 - 10h20 Tool development
09h00 iUML-B Statemachines
Colin Snook
09h20 EB2RC: A Rodin plug-in for visualising Event-B models and code generation
Zheng Cheng, Dominique Mery, Rosemary Monahan
09h40 Composition Operators for Event-B. CO4EB Rodin plugin
Idir Ait-Sadoune, Yamine Ait- Ameur
10h00 CODA Update: New Features for 2014
Neil Evans, Helen Marshall, James Sharp, Michael Butler, John Colley, Colin Snook
10h20 - 11h00 BREAK
11h00 - 11h40 Tool development
11h00 A Practical Approach for Validation with Rodin Theories
Daniel Plagge, Michael Leuschel
11h20 Rodin Multi-Simulation Plug-in
Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto
11h40 - 12h00 Teaching
11h40 Formal Methods, Requirements and Software Engineering
Ken Robinson
12h00 - 12h20 Theory
12h00 Responsiveness and Event-B
James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook
12h20 - 14h00 LUNCH
14h00 - 15h20 Theory
14h00 Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events)
Jean-Raymond Abrial
14h20 Program Development in Event-B with Proof Outlines
Stefan Hallerstede
14h40 Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi
15h00 Smart Grids: Multi-Simulation, An Application
Brett Bicknell, Karim Kanso, Jose Reis
15h20 - 16h00 BREAK
16h00 - 17h40 Theory
16h00 Towards Patterns for Statemachine Modelling under Timing Constraints
Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh
16h20 From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B
John Colley, Michael Butler
16h40 Event-B for Safety Analysis of Critical Systems
Matthias Gudemann and Marielle Petit-Doche
17h00 Modelling Of Systems Of Systems - An Event-B Perspective Of a VDM Project
Stefan Hallerstede , Klaus Kristensen, Peter Gorm Larsen

Organisers

Michael Butler, University of Southampton

Stefan Hallerstede, Aarhus University

Thierry Lecomte, ClearSy

Michael Leuschel, University of Düsseldorf

Alexander Romanovsky, Newcastle University

Laurent Voisin, Systerel

Marina Walden, Åbo Akademi University

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