Difference between revisions of "Rewriting rules for event model decomposition"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 16: Line 16:
 
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>
 
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>
 
|-
 
|-
|<math>v,w \bcmeq E,F</math>||<math>v \bcmeq E \pprod w \bcmeq F</math>
+
|<math>v \bcmeq E \pprod w \bcmeq F</math>||<math>v,w \bcmeq E,F</math>
 
|-
 
|-
 
|<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>
 
|<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>
Line 31: Line 31:
  
 
== Rewriting rules on Event-B actions ==
 
== Rewriting rules on Event-B actions ==
Let <math>v</math> and <math>w</math> be variables, and  <math>P</math> and <math>Q</math> be predicates. The following equivalence applies:
+
Let <math>v</math> and <math>w</math> be variables, <math>E</math> and <math>F</math> be expressions, and  <math>P</math> and <math>Q</math> be predicates. The left-hand actions are equivalent to the right-hand ones:
 
+
{{SimpleHeader}}
{|
+
|-
|<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</math>||&nbsp;&nbsp;&nbsp;&nbsp;<math>\defi\;\; v,w \bcmsuch P(v,v') \land Q(w,w')</math>
+
|<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</math>||<math>v,w \bcmsuch P(v,v') \land Q(w,w')</math>
 +
|-
 +
|<math>v,w \bcmeq E,F</math>||<math>v~ \bcmeq E</math><br><math>w \bcmeq F</math>
 
|}
 
|}
  
 
== Simplification rules based on Event-B proof obligations ==
 
== Simplification rules based on Event-B proof obligations ==

Revision as of 10:29, 3 July 2009

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.

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).

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 based on Event-B proof obligations