imported>Josselin |
|
Line 1: |
Line 1: |
− | Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
| + | {{TOCright}} |
− | Rules without a <tt>*</tt> are planned to be implemented in future versions.
| + | Return to [[Rodin Plug-ins]] |
− | Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
| |
| | | |
− | {{RRHeader}}
| + | The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. |
− | {{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>|| where <math>x</math> is not free in <math>S</math> || M
| + | Extension to Event-B including the ''machine inclusion'' mechanism is also supported. |
− | {{RRRow}}|||{{Rulename|SIMP_SETENUM_EQUAL_EMPTY}}||<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math>|| || A
| |
− | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_POW_EQUAL_EMPTY}}||<math> \pow (S) = \emptyset \;\;\defi\;\; \bfalse </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math> (\Union x\qdot P(x) \mid E(x)) = \emptyset \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \emptyset</math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_NATURAL_EQUAL_EMPTY}}||<math> \nat = \emptyset \;\;\defi\;\; \bfalse</math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_NATURAL1_EQUAL_EMPTY}}||<math> \natn = \emptyset \;\;\defi\;\; \bfalse</math>|| || A
| |
− | {{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_EMPTY}}||<math> S \cprod T \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math> i \upto j \;\;\defi\;\; i > j </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 operator <math>\tfun</math> || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math> A \srel B \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math> A \strel B \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_DOM_EQUAL_EMPTY}}||<math> \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_RAN_EQUAL_EMPTY}}||<math> \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_FCOMP_EQUAL_EMPTY}}||<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_BCOMP_EQUAL_EMPTY}}||<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_EMPTY}}||<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_RELIMAGE_EQUAL_EMPTY}}||<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_OVERL_EQUAL_EMPTY}}||<math> r \ovl \ldots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \ldots \land s = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_EMPTY}}||<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_EMPTY}}||<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_ID_EQUAL_EMPTY}}||<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>|| || A
| |
− | {{RRRow}}|||{{Rulename|SIMP_PRJ2_EQUAL_EMPTY}}||<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>|| || A
| |
− | |}
| |
| | | |
| + | <br style="clear: both" /> |
| | | |
− | [[Category:User documentation|The Proving Perspective]] | + | Please have a look also at the [[CamilleX User Guide]]. |
− | [[Category:Rodin Platform|The Proving Perspective]]
| + | |
− | [[Category:User manual|The Proving Perspective]]
| + | === 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. |