imported>Pascal |
imported>Stefan |
| Line 1: |
Line 1: |
| − | 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. | + | The Developer Support provides resources for developing plug-ins for the Rodin Platform. |
| | | | |
| − | == Equivalence relation ==
| + | [[Category:Developer Documentation]] |
| − | 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.
| + | [[Category:Rodin Platform]] |
| | | | |
| − | This relation is represented with the <math>\equiv</math> symbol.
| + | == Rodin Core == |
| | | | |
| − |
| + | [[Database]] |
| | | | |
| − | == Rewriting rules on Event-B assignments ==
| + | [[Builder]] |
| − | As detailed in [[Actions_(Modelling_Language)|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:
| + | == Event-B User Interface == |
| − | * 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 <math>\bcmeq</math> ("becomes equal to") assignment is the deterministic assignment where an expression is given for each 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 (<math>\equiv</math>) to the right-hand ones:
| + | [[Editing]] |
| − | {{SimpleHeader}}
| |
| − | |-
| |
| − | |<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>||<font id="rule_1">Rule 1</font>
| |
| − | |-
| |
| − | |<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>||<font id="rule_2">Rule 2</font>
| |
| − | |-
| |
| − | |<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>||<font id="rule_3">Rule 3</font>
| |
| − | |}
| |
| | | | |
| − | Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as <math>v_1,...,v_n \bcmsuch P(v_1,...v_n,v_1',...v_n')</math>, where <math>P</math> is a before-after predicate.
| + | [[Proving]] |
| | | | |
| − | == Rewriting rules on Event-B actions == | + | == Event-B Library == |
| − | 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 (<math>\equiv</math>) to the right-hand ones:
| |
| − | {{SimpleHeader}}
| |
| − | |-
| |
| − | |<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>||<font id="rule_4">Rule 4</font>
| |
| − | |-
| |
| − | |<math>v,w \bcmeq E,F</math>||<math>v~ \bcmeq E</math><br><math>w \bcmeq F</math>||<font id="rule_5">Rule 5</font>
| |
| − | |}
| |
| | | | |
| − | == Simplification rules on Event-B predicates ==
| + | [[Abstract Syntax Tree]] |
| − | Let <math>x_i</math>, <math>y</math> and <math>z</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
| |
| − | * <font id="rule_6">Rule 6</font>: If <math>P(x_1,...,x_n,y)~</math> is equal to <math>y = Q(x_1,...,x_n)~</math>, then the <math>\exists y.P(x1,...,x_n,y)</math> predicate is true, and it may be deleted in conjunctive predicates (<math>\land</math>) where it appears.
| |
| − | * <font id="rule_7">Rule 7</font>: The <math>(\exists z.P(x_1,...,x_n,z) \land Q(y_1,...,y_m))</math> predicate, where <math>z \notin \{y_1,...,y_n\}</math>, may be rewritten as <math>(\exists z.P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)</math>.
| |
| | | | |
| − | == Simplification rules based on Event-B proof obligations ==
| + | [[Static Checker]] |
| | | | |
| − | == Example ==
| + | [[Proof Obligation Generator]] |
| − | Let <math>a</math>, <math>b</math> and <math>x</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
| |
| − | {|
| |
| − | |-
| |
| − | |<math>a,b \bcmsuch \exists x.P(a,a',x) \land Q(b,b')</math>
| |
| − | |-
| |
| − | |<center><math>\equiv</math> [[#rule_7|(Rule 7)]]</center>
| |
| − | |-
| |
| − | |<math>a,b \bcmsuch (\exists x.P(a,a',x)) \land Q(b,b')</math>
| |
| − | |-
| |
| − | |<center><math>\equiv</math> [[#rule_4|(Rule 4)]]</center>
| |
| − | |-
| |
| − | |<math>a \bcmsuch \exists x.P(a,a',x)</math><br><math>b \bcmsuch Q(b,b')</math>
| |
| − | |}
| |
