Event-B Indexers: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Nicolas
imported>Nicolas
m →‎What Is Indexed: Added root elements indexing
 
(20 intermediate revisions by 3 users not shown)
Line 10: Line 10:
So far, the following occurrence kinds have been defined :
So far, the following occurrence kinds have been defined :
* DECLARATION : when a variable, a carrier set, ..., is declared
* DECLARATION : when a variable, a carrier set, ..., is declared
* REFERENCE : when a variable, ..., is referenced (but not modified); also applies when an abstract element is redeclared in a refinement
* REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
* MODIFICATION : when a variable is 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.
Please notice the distinction between the index repository notion of declaration ({{class|IDeclaration}}) and the Event-B occurrence kind DECLARATION.


==What Indexers Index==
==What Is Indexed==


Currently, indexed elements are :
Currently, indexed elements are :
* root elements
* carrier sets
* carrier sets
* constants
* constants
Line 37: Line 38:


====Declarations====
====Declarations====
* context root
* carrier sets
* carrier sets
* constants
* constants
Line 42: Line 44:
====Occurrences====
====Occurrences====


* DECLARATION of carrier sets [Root]
* DECLARATION of context root [root] (occurrence in root itself)
* DECLARATION of constants [Root]
* DECLARATION of carrier sets [CarrierSet/Identifier]
* DECLARATION of constants [Constant/Identifier]
* REFERENCE of root elements in extends [Extends/Target]
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]


Example:
Example:
Line 60: Line 63:


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


====Exports====
====Exports====
* context root
* imported and declared carrier sets
* imported and declared carrier sets
* imported and declared constants
* imported and declared constants
Line 78: Line 81:


====Declarations====
====Declarations====
* machine root
* variables
* variables
* events
* events
Line 83: Line 87:


====Occurrences====
====Occurrences====
* DECLARATION of (local) variables [Root]
* DECLARATION of machine root [root] (occurrence in root itself)
* DECLARATION of (local) events [Root]
* DECLARATION of (local) variables [Variable/Identifier]
* DECLARATION of (local) parameters [Event]
* DECLARATION of (local) events [Event/Label]
* REFERENCE of abstract variables in the local variables that redeclare them [Variable/Identifier]
* DECLARATION of (local) parameters [Parameter/Identifier]
* REFERENCE of abstract events in the local events that refine them [RefinesEvent/Target]
* REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
* REFERENCE of abstract parameters in the local parameters that redeclare them [Parameter/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 root elements in refines [Refines/Target]
* REFERENCE of root elements in sees [Sees/Target]
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
* REFERENCE of elements in invariants [Invariant/Predicate/b..e]
* 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 variants [Variant/Expression/b..e]
* REFERENCE of elements in guards [Guard/Predicate/b..e]
* REFERENCE of elements in guards [Guard/Predicate/b..e]
Line 113: Line 119:


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


Then, if we add another machine
Then, if we add another machine
Line 134: Line 140:


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


====Exports====
====Exports====
* machine root
* imported carrier sets
* imported carrier sets
* imported constants
* imported constants
Line 148: Line 154:
* local events
* local events
* local parameters
* local parameters


==Propagation==
==Propagation==
Line 162: Line 167:


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


Using the {{class|IdentifierPropagator}}, the result becomes :
Using the {{class|IdentifierPropagator}}, the result becomes :


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


==Query Examples==
[[Category:Developer documentation]]
 
Here are a few examples of index queries. They are all implicitly preceded by the following code
 
 
  final IIndexQuery query = RodinCore.makeIndexQuery();
  query.waitUpToDate();
 
 
that makes the query and waits until the index becomes up-to-date.
 
 
===Occurrences of an element===
 
Data :
* a handle 'var' of an IVariable
 
To get its declaration
 
final IDeclaration declVar = query.getDeclaration(var);
 
From that declaration, the user-defined name of the variable can be retrieved
 
final String userDefinedName = declVar.getName();
 
To get the occurrences of 'var'
 
final Set<IOccurrence> occurrences = query.getOccurrences(declVar);
 
 
===Homonyms in a file===
 
Data :
* a handle 'file' of an {{class|IRodinFile}}
* a name "foo"
 
First, all declarations of all indexed elements that occur in 'file' are retrieved.
Then a query filter on the name is used.
 
final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterName(declarations, "foo");
 
At the end, 'declarations' contains the declarations of all elements named "foo" occurring in 'file'.
 
===Parameters of an event===
 
Data :
* a handle 'file' of an {{class|IRodinFile}}
* a handle 'evt1' of an {{class|IEvent}}
 
Goal :
getting the declarations of all parameters of 'evt1'
 
<pre>
final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterType(declarations, IParameter.ELEMENT_TYPE);
 
final Set<IOccurrence> occurrences = query.getOccurrences(declarations);
query.filterKind(occurrences, EventBPlugin.DECLARATION);
 
final IInternalLocation evt1Location = RodinCore.getInternalLocation(evt1);
query.filterLocation(occurrences, evt1Location);
 
final Set<IDeclaration> paramsOfEvt1 = query.getDeclarations(occurrences);
</pre>
 
We first get all declarations of elements that occur in 'file', and we filter them so as to keep only declarations of parameters.
We then get all occurrences of those parameters. We want parameters that have a DECLARATION occurrence in 'evt'. To that aim, two filters are successively applied to the occurrences. Finally we get the declarations ({{class|IDeclaration}} this time) that correspond to the filtered occurrences.
 
 
 
===Query with propagation===
 
{{TODO|add query examples}}

Latest revision as of 22:36, 11 July 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 :

  • root elements
  • 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

  • context root
  • carrier sets
  • constants

Occurrences

  • DECLARATION of context root [root] (occurrence in root itself)
  • DECLARATION of carrier sets [CarrierSet/Identifier]
  • DECLARATION of constants [Constant/Identifier]
  • REFERENCE of root elements in extends [Extends/Target]
  • REFERENCE of elements in axioms [Axiom/Predicate/b..e]

Example: 

 Ctx
 Sets
   S
 Constants
   C
 Axioms
   axm1 : C ∈ S

We will end up with the following occurrences : 

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

Exports

  • context root
  • imported and declared carrier sets
  • imported and declared constants

Machine Indexer

Dependencies

  • refined machines
  • seen contexts

Declarations

  • machine root
  • variables
  • events
  • parameters

Occurrences

  • DECLARATION of machine root [root] (occurrence in root itself)
  • DECLARATION of (local) variables [Variable/Identifier]
  • DECLARATION of (local) events [Event/Label]
  • DECLARATION of (local) parameters [Parameter/Identifier]
  • 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 root elements in refines [Refines/Target]
  • REFERENCE of root elements in sees [Sees/Target]
  • REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
  • REFERENCE of elements in invariants [Invariant/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.var1/Identifier]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
 M1.INITIALISATION :
   DECLARATION in [M1.INITIALISATION/Label]

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.var1/Identifier]
   MODIFICATION in [M2.act1/Assignment/0..4]
 M2.INITIALISATION :
   DECLARATION in [M2.INITIALISATION/Label]

Exports

  • machine root
  • 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.var1/Identifier]
   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.var1/Identfiier]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
   REDECLARATION in [M2.var1/Identifier]
   DECLARATION in [M2.var1/Identifier]
   MODIFICATION in [M2.act1/Assignment/0..4]
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Indexers&oldid=4122’