Difference between revisions of "Arithmetic Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Tommy m (removed * on unimplemented rules) |
imported>Tommy m (removed * on unimplemented rules - 2nd pass) |
||
Line 10: | Line 10: | ||
{{RRRow}}|||{{Rulename|SIMP_MIN_UPTO}}||<math> \min (E \upto F) \;\;\defi\;\; E </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_MIN_UPTO}}||<math> \min (E \upto F) \;\;\defi\;\; E </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MAX_UPTO}}||<math> \max (E \upto F) \;\;\defi\;\; F </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_MAX_UPTO}}||<math> \max (E \upto F) \;\;\defi\;\; F </math>|| || A | ||
− | {{RRRow}}| | + | {{RRRow}}|||{{Rulename|SIMP_LIT_MIN}}||<math> \min (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \min (\{ E, \ldots , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> || A |
{{RRRow}}|||{{Rulename|SIMP_LIT_MAX}}||<math> \max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> || A | {{RRRow}}|||{{Rulename|SIMP_LIT_MAX}}||<math> \max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> || A | ||
{{RRRow}}|||{{Rulename|SIMP_LIT_MIN_UPTO}}||<math> \min (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals || A | {{RRRow}}|||{{Rulename|SIMP_LIT_MIN_UPTO}}||<math> \min (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals || A | ||
Line 30: | Line 30: | ||
{{RRRow}}|||{{Rulename|SIMP_LIT_LE_CARD_1}}||<math> 1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_LIT_LE_CARD_1}}||<math> 1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_LIT_LE_CARD_0}}||<math> 0 \leq \card (S) \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_LIT_LE_CARD_0}}||<math> 0 \leq \card (S) \;\;\defi\;\; \btrue </math>|| || A | ||
− | {{RRRow}}| | + | {{RRRow}}|||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math> \card (S) \geq 0 \;\;\defi\;\; \btrue </math>|| || A |
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT_CARD_0}}||<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_LIT_GT_CARD_0}}||<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_LIT_LT_CARD_0}}||<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_LIT_LT_CARD_0}}||<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A |
Revision as of 11:09, 21 December 2009
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
SIMP_SPECIAL_MOD_0 |
![]() |
A | ||
SIMP_SPECIAL_MOD_1 |
![]() |
A | ||
SIMP_MIN_SING |
![]() |
where ![]() |
A | |
SIMP_MAX_SING |
![]() |
where ![]() |
A | |
SIMP_MIN_NATURAL |
![]() |
A | ||
SIMP_MIN_NATURAL1 |
![]() |
A | ||
SIMP_MIN_BUNION_SING |
![]() |
A | ||
SIMP_MAX_BUNION_SING |
![]() |
A | ||
SIMP_MIN_UPTO |
![]() |
A | ||
SIMP_MAX_UPTO |
![]() |
A | ||
SIMP_LIT_MIN |
![]() |
where ![]() ![]() ![]() |
A | |
SIMP_LIT_MAX |
![]() |
where ![]() ![]() ![]() |
A | |
SIMP_LIT_MIN_UPTO |
![]() |
where ![]() |
A | |
SIMP_LIT_MAX_UPTO |
![]() |
where ![]() |
A | |
* | SIMP_SPECIAL_CARD |
![]() |
A | |
* | SIMP_CARD_SING |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_EQUAL_CARD |
![]() |
A | |
* | SIMP_CARD_POW |
![]() |
A | |
* | SIMP_CARD_BUNION |
![]() |
A | |
* | SIMP_CARD_SETMINUS |
![]() |
A | |
* | SIMP_CARD_CPROD |
![]() |
A | |
SIMP_CARD_CONVERSE |
![]() |
A | ||
SIMP_CARD_ID |
![]() |
A | ||
SIMP_CARD_LAMBDA |
![]() |
A | ||
SIMP_CARD_COMPSET |
![]() |
where ![]() ![]() |
A | |
* | SIMP_LIT_CARD_UPTO |
![]() |
where ![]() ![]() ![]() |
A |
SIMP_TYPE_CARD |
![]() |
where ![]() ![]() |
A | |
SIMP_LIT_GE_CARD_0 |
![]() |
A | ||
SIMP_LIT_LE_CARD_1 |
![]() |
A | ||
SIMP_LIT_LE_CARD_0 |
![]() |
A | ||
SIMP_LIT_GE_CARD_0 |
![]() |
A | ||
* | SIMP_LIT_GT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_LT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_EQUAL_CARD_1 |
![]() |
A | |
SIMP_CARD_NATURAL |
![]() |
A | ||
SIMP_CARD_NATURAL1 |
![]() |
A | ||
SIMP_LIT_IN_NATURAL |
![]() |
where ![]() |
A | |
SIMP_SPECIAL_IN_NATURAL1 |
![]() |
A | ||
SIMP_LIT_IN_NATURAL1 |
![]() |
where ![]() ![]() |
A | |
SIMP_LIT_UPTO |
![]() |
where ![]() ![]() ![]() |
A | |
SIMP_LIT_IN_MINUS_NATURAL |
![]() |
where ![]() ![]() |
A | |
SIMP_LIT_IN_MINUS_NATURAL1 |
![]() |
where ![]() |
A | |
DEF_IN_NATURAL |
![]() |
where ![]() ![]() |
A | |
DEF_IN_NATURAL1 |
![]() |
where ![]() ![]() |
A | |
SIMP_SPECIAL_KBOOL_BTRUE |
![]() |
A | ||
SIMP_SPECIAL_KBOOL_BFALSE |
![]() |
A | ||
* | SIMP_LIT_EQUAL_KBOOL_TRUE |
![]() |
A | |
* | SIMP_LIT_EQUAL_KBOOL_FALSE |
![]() |
A | |
DEF_EQUAL_MIN |
![]() |
where ![]() ![]() |
M | |
DEF_EQUAL_MAX |
![]() |
where ![]() ![]() |
M | |
* | SIMP_SPECIAL_PLUS |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_R |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_L |
![]() |
A | |
* | SIMP_MINUS_MINUS |
![]() |
A | |
* | SIMP_MINUS_UNMINUS |
![]() |
where ![]() |
M |
* | SIMP_MULTI_MINUS |
![]() |
A | |
* | SIMP_MULTI_MINUS_PLUS_L |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_R |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_PLUS |
![]() |
M | |
* | SIMP_MULTI_PLUS_MINUS |
![]() |
M | |
* | SIMP_MULTI_ARITHREL_PLUS_PLUS |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_SPECIAL_PROD_0 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_1 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_MINUS_EVEN |
![]() |
if an even number of ![]() |
A |
* | SIMP_SPECIAL_PROD_MINUS_ODD |
![]() |
if an odd number of ![]() |
A |
SIMP_LIT_MINUS |
![]() |
where ![]() |
A | |
SIMP_LIT_MINUS_MINUS |
![]() |
where ![]() |
A | |
* | SIMP_LIT_EQUAL |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LT |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GT |
![]() |
where ![]() ![]() |
A |
* | SIMP_DIV_MINUS |
![]() |
A | |
SIMP_SPECIAL_DIV_1 |
![]() |
A | ||
* | SIMP_SPECIAL_DIV_0 |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_R |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_L |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_0 |
![]() |
A | |
* | SIMP_MULTI_LE |
![]() |
A | |
* | SIMP_MULTI_LT |
![]() |
A | |
* | SIMP_MULTI_GE |
![]() |
A | |
* | SIMP_MULTI_GT |
![]() |
A | |
* | SIMP_MULTI_DIV |
![]() |
A | |
* | SIMP_MULTI_DIV_PROD |
![]() |
A | |
SIMP_MULTI_MOD |
![]() |
A | ||
DISTRI_PROD_PLUS |
![]() |
M | ||
DISTRI_PROD_MINUS |
![]() |
M | ||
* | DERIV_LE_CARD |
![]() |
![]() ![]() |
M |
* | DERIV_GE_CARD |
![]() |
![]() ![]() |
M |
* | DERIV_LT_CARD |
![]() |
![]() ![]() |
M |
* | DERIV_GT_CARD |
![]() |
![]() ![]() |
M |
* | DERIV_EQUAL_CARD |
![]() |
![]() ![]() |
M |
DERIV_NOT_EQUAL |
![]() |
![]() ![]() |
M |