Rewriting rules for event model decomposition

The purpose of this page is to list and justify the rewriting / simplification rules applied in the event model decomposition when building the external events, and more especially their actions.

Rewriting rules on Event-B assignments

As detailed in the modelling language, the Event-B assignments are formed of two parts:

• a left-hand side, which is a list of free identifiers.
• a right-hand side.

There are various kinds of assignments:

• The $\bcmsuch$ ("becomes such that") assignment is the most general (non-deterministic) assignment, where a predicate is given on the before and after values of assigned identifiers. The after values of the assigned identifiers are denoted by a primed identifier whose prefix is the assigned identifier.
• The $\bcmeq$ ("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
• The $\bcmin$ ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.

Let $v$ and $w$ be variables, and $E$ and $F$ be expressions. In the following table, the left-hand assignments are equivalent to the right-hand ones:

$v \bcmeq E$	$v \bcmsuch v' = E$
$v \bcmeq E \pprod w \bcmeq F$	$v,w \bcmeq E,F$
$v(E) \bcmeq F$	$v \bcmeq v \ovl \{E \mapsto F\}$
$v \bcmin E$	$v \bcmsuch v' \in E$

Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as $v_1,...,v_n \bcmsuch P(v_1,...v_n,v_1',...v_n')$, where $P$ is a before-after predicate.

Rewriting rules on Event-B actions

Let $v$ and $w$ be variables, $E$ and $F$ be expressions, and $P$ and $Q$ be predicates. The left-hand actions are equivalent to the right-hand ones:

$v~ \bcmsuch P(v,v')$ $w \bcmsuch Q(w,w')$	$v,w \bcmsuch P(v,v') \land Q(w,w')$
$v,w \bcmeq E,F$	$v~ \bcmeq E$ $w \bcmeq F$

Simplification rules on Event-B predicates

Let $x_i$, $y$ and $z$ be variables, and $P$ and $Q$ be predicates.

• If $P(x_1,...,x_n,y)~$ is equal to $y = Q(x_1,...,x_n)~$, then the $\exists y.P(x1,...,x_n,y)$ predicate is true, and it may be deleted in conjunctive predicates ($\land$) where it appears.
• The $(\exists z.P(x_1,...,x_n,z) \land Q(y_1,...,y_m))$ predicate, where $z \notin \{y_1,...,y_n\}$, may be rewritten as $(\exists z.P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)$.