Rewriting rules for event model decomposition
From Event-B
Revision as of 16:02, 2 July 2009 by imported>Pascal (Rewriting rules moved to Rewriting rules for event model decomposition)
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 "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,
is the deterministic assignment, where an expression is given for each assigned identifier.
- The "becomes member of" assignment,
is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
Let and
be variables, and
and
be expressions. In the following table, the left-hand assignments are equivalent (\defi) to the right-hand ones:
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
Thus, each Event-B assignment can be expressed in a "becomes such that" form.