Difference between pages "Empty Set Rewrite Rules" and "Event-B Indexers"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Josselin
(Fixed rule SIMP_SREL_EQUAL_EMPTY)
 
imported>Laurent
 
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
==Purpose==
Rules without a <tt>*</tt> are planned to be implemented in future versions.
 
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 
  
{{RRHeader}}
+
Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :
{{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math>  \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S </math>|| where <math>x</math> is not free in <math>S</math> ||  M
+
* machine (.bum)
{{RRRow}}|||{{Rulename|SIMP_SETENUM_EQUAL_EMPTY}}||<math>  \{ A, \ldots , B\}  = \emptyset \;\;\defi\;\;  \bfalse </math>||  ||  A
+
* context (.buc)
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math>  \{  x \qdot  P(x) \mid  E \}  = \emptyset  \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math>  A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\;  A = \emptyset \land \ldots \land B  = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math>  A \setminus  B = \emptyset \;\;\defi\;\;  A \subseteq  B  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_POW_EQUAL_EMPTY}}||<math>  \pow (S) = \emptyset \;\;\defi\;\;  \bfalse  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math>  \pown (S) = \emptyset \;\;\defi\;\;  S = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math>  \union (S) = \emptyset \;\;\defi\;\;  S \subseteq \{ \emptyset \}  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math>  (\Union  x\qdot P(x)  \mid  E(x)) = \emptyset \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \emptyset</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_NATURAL_EQUAL_EMPTY}}||<math>  \nat = \emptyset \;\;\defi\;\;  \bfalse</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_NATURAL1_EQUAL_EMPTY}}||<math>  \natn = \emptyset \;\;\defi\;\;  \bfalse</math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_EMPTY}}||<math>  S \cprod T \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math>  i \upto j \;\;\defi\;\; i > j </math>|| ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math>  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse </math>|| idem for operators <math>\pfun  \pinj</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math>  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset </math>|| idem for operator <math>\tfun</math> ||  A
 
{{RRRow}}|||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math>  A \srel B \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math>  A \strel B \;\;\defi\;\; (A = \emptyset \;\;\defi\;\;  \lnot\,B = \emptyset) </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_DOM_EQUAL_EMPTY}}||<math>  \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RAN_EQUAL_EMPTY}}||<math>  \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_FCOMP_EQUAL_EMPTY}}||<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_BCOMP_EQUAL_EMPTY}}||<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_EMPTY}}||<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset  </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RELIMAGE_EQUAL_EMPTY}}||<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_OVERL_EQUAL_EMPTY}}||<math>  r \ovl \ldots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \ldots \land s =  \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_EMPTY}}||<math>  p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_EMPTY}}||<math>  p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_ID_EQUAL_EMPTY}}||<math>  \id = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math>  \prjone = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_PRJ2_EQUAL_EMPTY}}||<math>  \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
|}
 
  
  
[[Category:User documentation|The Proving Perspective]]
+
==Event-B Occurrence Kinds==
[[Category:Rodin Platform|The Proving Perspective]]
+
 
[[Category:User manual|The Proving Perspective]]
+
So far, the following occurrence kinds have been defined :
 +
* DECLARATION : when a variable, a carrier set, ..., is declared
 +
* REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
 +
* MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
 +
* REDECLARATION : when a variable, parameter or event is redeclared (refined).
 +
Please notice the distinction between the index repository notion of declaration ({{class|IDeclaration}}) and the Event-B occurrence kind DECLARATION.
 +
 
 +
==What Is Indexed==
 +
 
 +
Currently, indexed elements are :
 +
* carrier sets
 +
* constants
 +
* variables
 +
* events
 +
* parameters
 +
 
 +
Formulas which cannot be parsed are ignored.
 +
 
 +
In the descriptions below, the following notation will be used to specify locations :
 +
* [element] : internal location
 +
* [element/attribute] : attribute location
 +
* [element/attribute/begin..end] : attribute substring location
 +
 
 +
===Context Indexer===
 +
 
 +
====Dependencies====
 +
* extended contexts
 +
 
 +
====Declarations====
 +
* carrier sets
 +
* constants
 +
 
 +
====Occurrences====
 +
 
 +
* DECLARATION of carrier sets [CarrierSet/Identifier]
 +
* DECLARATION of constants [Constant/Identifier]
 +
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
 +
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 +
 
 +
Example:
 +
 
 +
  Ctx
 +
  Sets
 +
    S
 +
  Constants
 +
    C
 +
  Axioms
 +
    axm1 : C ∈ S
 +
 
 +
We will end up with the following occurrences :
 +
 
 +
  S :
 +
    DECLARATION in [Ctx.Root]
 +
    REFERENCE in [axm1/Predicate/4..5]
 +
  C :
 +
    DECLARATION in [Ctx.Root]
 +
    REFERENCE in [axm1/Predicate/0..1]
 +
 
 +
====Exports====
 +
* imported and declared carrier sets
 +
* imported and declared constants
 +
 
 +
===Machine Indexer===
 +
 
 +
====Dependencies====
 +
* refined machines
 +
* seen contexts
 +
 
 +
====Declarations====
 +
* variables
 +
* events
 +
* parameters
 +
 
 +
====Occurrences====
 +
* DECLARATION of (local) variables [Root]
 +
* DECLARATION of (local) events [Root]
 +
* DECLARATION of (local) parameters [Event]
 +
* REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
 +
* REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
 +
* REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
 +
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
 +
* REFERENCE of elements in invariants [Invariant/Predicate/b..e]
 +
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 +
* REFERENCE of elements in variants [Variant/Expression/b..e]
 +
* REFERENCE of elements in guards [Guard/Predicate/b..e]
 +
* REFERENCE of elements in witnesses [Witness/Predicate/b..e]
 +
* REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
 +
* MODIFICATION of assigned elements in actions [Action/Assignment/b..e]
 +
 
 +
Example :
 +
 
 +
  M1
 +
  VARIABLES
 +
    var1
 +
  INVARIANTS
 +
    inv1 : var1 > 0
 +
  EVENTS
 +
    INITIALISATION
 +
      THEN
 +
        act1 : var1 := 1
 +
 
 +
After indexing M1, we will have the following occurrences:
 +
 
 +
  M1.var1 :
 +
    DECLARATION in [M1.Root]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
  M1.INITIALISATION :
 +
    DECLARATION in [M1.Root]
 +
 
 +
Then, if we add another machine
 +
 
 +
  M2
 +
  REFINES
 +
    M1
 +
  VARIABLES
 +
    var1
 +
  EVENTS
 +
    INITIALISATION
 +
      THEN
 +
        act1 : var1 := 1
 +
 
 +
we will add the following occurrences :
 +
 
 +
  M1.var1 :
 +
    REDECLARATION in [M2.var1/Identifier]
 +
  M2.var1 :
 +
    DECLARATION in [M2.Root]
 +
    MODIFICATION in [M2.act1/Assignment/0..4]
 +
  M2.INITIALISATION :
 +
    DECLARATION in [M2.Root]
 +
 
 +
====Exports====
 +
* imported carrier sets
 +
* imported constants
 +
* local variables
 +
* local events
 +
* local parameters
 +
 
 +
==Propagation==
 +
 
 +
Propagators are defined for :
 +
* events ({{class|EventPropagator}}) to propagate through refines
 +
* parameters ({{class|IdentifierPropagator}}) to propagate through redeclaration
 +
* variables ({{class|IdentifierPropagator}} as well) to propagate through redeclaration
 +
 
 +
In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.
 +
 
 +
With no propagator, the result would be :
 +
 
 +
  M1.var1 :
 +
    DECLARATION in [M1.Root]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
    REDECLARATION in [M2.var1/Identifier]
 +
 
 +
Using the {{class|IdentifierPropagator}}, the result becomes :
 +
 
 +
  M1.var1 (propagated) :
 +
    DECLARATION in [M1.Root]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
    REDECLARATION in [M2.var1/Identifier]
 +
    DECLARATION in [M2.Root]
 +
    MODIFICATION in [M2.act1/Assignment/0..4]
 +
 
 +
[[Category:Developer documentation]]

Revision as of 09:39, 10 March 2009

Purpose

Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :

  • machine (.bum)
  • context (.buc)


Event-B Occurrence Kinds

So far, the following occurrence kinds have been defined :

  • DECLARATION : when a variable, a carrier set, ..., is declared
  • REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
  • MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
  • REDECLARATION : when a variable, parameter or event is redeclared (refined).

Please notice the distinction between the index repository notion of declaration (IDeclaration) and the Event-B occurrence kind DECLARATION.

What Is Indexed

Currently, indexed elements are :

  • carrier sets
  • constants
  • variables
  • events
  • parameters

Formulas which cannot be parsed are ignored.

In the descriptions below, the following notation will be used to specify locations :

  • [element] : internal location
  • [element/attribute] : attribute location
  • [element/attribute/begin..end] : attribute substring location

Context Indexer

Dependencies

  • extended contexts

Declarations

  • carrier sets
  • constants

Occurrences

  • DECLARATION of carrier sets [CarrierSet/Identifier]
  • DECLARATION of constants [Constant/Identifier]
  • REFERENCE of elements in axioms [Axiom/Predicate/b..e]
  • REFERENCE of elements in theorems [Theorem/Predicate/b..e]

Example:

 Ctx
 Sets
   S
 Constants
   C
 Axioms
   axm1 : C ∈ S

We will end up with the following occurrences :

 S :
   DECLARATION in [Ctx.Root]
   REFERENCE in [axm1/Predicate/4..5]
 C :
   DECLARATION in [Ctx.Root]
   REFERENCE in [axm1/Predicate/0..1]

Exports

  • imported and declared carrier sets
  • imported and declared constants

Machine Indexer

Dependencies

  • refined machines
  • seen contexts

Declarations

  • variables
  • events
  • parameters

Occurrences

  • DECLARATION of (local) variables [Root]
  • DECLARATION of (local) events [Root]
  • DECLARATION of (local) parameters [Event]
  • REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
  • REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
  • REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
  • REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
  • REFERENCE of elements in invariants [Invariant/Predicate/b..e]
  • REFERENCE of elements in theorems [Theorem/Predicate/b..e]
  • REFERENCE of elements in variants [Variant/Expression/b..e]
  • REFERENCE of elements in guards [Guard/Predicate/b..e]
  • REFERENCE of elements in witnesses [Witness/Predicate/b..e]
  • REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
  • MODIFICATION of assigned elements in actions [Action/Assignment/b..e]

Example :

 M1
 VARIABLES
   var1
 INVARIANTS
   inv1 : var1 > 0
 EVENTS
   INITIALISATION
     THEN
       act1 : var1 := 1

After indexing M1, we will have the following occurrences:

 M1.var1 :
   DECLARATION in [M1.Root]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
 M1.INITIALISATION :
   DECLARATION in [M1.Root]

Then, if we add another machine

 M2
 REFINES
   M1
 VARIABLES
   var1
 EVENTS
   INITIALISATION
     THEN
       act1 : var1 := 1

we will add the following occurrences :

 M1.var1 :
   REDECLARATION in [M2.var1/Identifier]
 M2.var1 :
   DECLARATION in [M2.Root]
   MODIFICATION in [M2.act1/Assignment/0..4]
 M2.INITIALISATION :
   DECLARATION in [M2.Root]

Exports

  • imported carrier sets
  • imported constants
  • local variables
  • local events
  • local parameters

Propagation

Propagators are defined for :

  • events (EventPropagator) to propagate through refines
  • parameters (IdentifierPropagator) to propagate through redeclaration
  • variables (IdentifierPropagator as well) to propagate through redeclaration

In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.

With no propagator, the result would be :

 M1.var1 :
   DECLARATION in [M1.Root]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
   REDECLARATION in [M2.var1/Identifier]

Using the IdentifierPropagator, the result becomes :

 M1.var1 (propagated) :
   DECLARATION in [M1.Root]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
   REDECLARATION in [M2.var1/Identifier]
   DECLARATION in [M2.Root]
   MODIFICATION in [M2.act1/Assignment/0..4]