Difference between revisions of "Rewriting rules for event model decomposition"
imported>Pascal m |
imported>Pascal |
||
Line 15: | Line 15: | ||
|- | |- | ||
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math> | |<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</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> |
Revision as of 10:38, 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.
Contents
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
("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 to the right-hand ones:
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as , where
is a before-after predicate.
Rewriting rules on Event-B actions
Let and
be variables,
and
be expressions, and
and
be predicates. The left-hand actions are equivalent to the right-hand ones:
![]() ![]() |
![]() |
![]() |
![]() ![]() |
Simplification rules on Event-B predicates
Let ,
and
be variables, and
and
be predicates.
- If
is equal to
, then the
predicate is true, and it may be deleted in conjunctive predicates (
) where it appears.
- The
predicate, where
, may be rewritten as
.