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.

Equivalence relation

It is possible to define an equivalence relation on the Event-B actions, and by restrictions on the Event-B assignments (an action is a set of assignments). Two actions are considered as being equivalent if the proof obligations generated for these actions are logically equivalent.

This relation is represented with the $\defi$ symbol.

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 ($\defi$) to the right-hand ones (see the B-book):

$v \bcmeq E$	$v \bcmsuch v' = E$	Rule 1
$v(E) \bcmeq F$	$v \bcmeq v \ovl \{E \mapsto F\}$	Rule 2
$v \bcmin E$	$v \bcmsuch v' \in E$	Rule 3

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 ($\defi$) to the right-hand ones:

$\begin{array}{ll}v\!\!\! &\bcmsuch P(v,v')\\ w\!\!\! &\bcmsuch Q(w,w') \end{array}$	$v,w \bcmsuch P(v,v') \land Q(w,w')$	Rule 4
$v,w \bcmeq E,F$	$\begin{array}{ll}v\!\!\! &\bcmeq E\\ w\!\!\! &\bcmeq F \end{array}$	Rule 5

Simplification rules on Event-B predicates

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

• Rule 6: 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.
• Rule 7: 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)$.

Simplification rules based on Event-B proof obligations

TO BE COMPLETED

Example

Let $a$, $b$ and $x$ be variables, and $P$ and $Q$ be predicates.

$a,b \bcmsuch \exists x \qdot P(a,a',x) \land Q(b,b')$

$\defi$ (Rule 7)

$a,b \bcmsuch (\exists x \qdot P(a,a',x)) \land Q(b,b')$

$\defi$ (Rule 4)

$\begin{array}{ll}a\!\!\! &\bcmsuch \exists x \qdot P(a,a',x)\\ b\!\!\! &\bcmsuch Q(b,b')\end{array}$