Rewriting rules for event model decomposition: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 7: Line 7:


There are various kinds of assignments:
There are various kinds of assignments:
* The "becomes such that" assignment, <math>\bcmsuch</math>, 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 <math>\bcmsuch</math> ("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 "becomes equal to" assignment, <math>\bcmeq</math> is the deterministic assignment, where an expression is given for each assigned identifier.
* The <math>\bcmeq</math> ("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
* The "becomes member of" assignment, <math>\bcmin</math> is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
* The <math>\bcmin</math> ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.


Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (\defi) to the right-hand ones:
Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (\defi) to the right-hand ones:

Revision as of 16:36, 2 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 for the 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:

v \bcmeq E v \bcmsuch v' = E
v,w \bcmeq E,F v \bcmeq E \pprod w \bcmeq 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.

Simplification rules on Event-B predicates

Rewriting rules for the Event-B actions

Simplification rules based on Event-B proof obligations