Event-B Indexers: Difference between revisions
imported>Laurent |
imported>Nicolas m →What Is Indexed: Added root elements indexing |
||
(7 intermediate revisions by 2 users not shown) | |||
Line 18: | Line 18: | ||
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 [ | * DECLARATION of context root [root] (occurrence in root itself) | ||
* DECLARATION of constants [ | * 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] | ||
Example: | Example: | ||
Line 60: | Line 63: | ||
S : | S : | ||
DECLARATION in [ | DECLARATION in [S/Identifier] | ||
REFERENCE in [axm1/Predicate/4..5] | REFERENCE in [axm1/Predicate/4..5] | ||
C : | C : | ||
DECLARATION in [ | 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 77: | Line 81: | ||
====Declarations==== | ====Declarations==== | ||
* machine root | |||
* variables | * variables | ||
* events | * events | ||
Line 82: | Line 87: | ||
====Occurrences==== | ====Occurrences==== | ||
* DECLARATION of (local) variables [ | * DECLARATION of machine root [root] (occurrence in root itself) | ||
* DECLARATION of (local) events [ | * DECLARATION of (local) variables [Variable/Identifier] | ||
* DECLARATION of (local) parameters [ | * 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 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 events in the local events that refine them [Event/RefinesEvent/Target] | ||
* REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier] | * 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 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 112: | Line 119: | ||
M1.var1 : | M1.var1 : | ||
DECLARATION in [M1. | 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. | DECLARATION in [M1.INITIALISATION/Label] | ||
Then, if we add another machine | Then, if we add another machine | ||
Line 135: | Line 142: | ||
REDECLARATION in [M2.var1/Identifier] | REDECLARATION in [M2.var1/Identifier] | ||
M2.var1 : | M2.var1 : | ||
DECLARATION in [M2. | 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. | DECLARATION in [M2.INITIALISATION/Label] | ||
====Exports==== | ====Exports==== | ||
* machine root | |||
* imported carrier sets | * imported carrier sets | ||
* imported constants | * imported constants | ||
Line 159: | Line 167: | ||
M1.var1 : | M1.var1 : | ||
DECLARATION in [M1. | 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] | ||
Line 167: | Line 175: | ||
M1.var1 (propagated) : | M1.var1 (propagated) : | ||
DECLARATION in [M1. | 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] | ||
REDECLARATION in [M2.var1/Identifier] | REDECLARATION in [M2.var1/Identifier] | ||
DECLARATION in [M2. | DECLARATION in [M2.var1/Identifier] | ||
MODIFICATION in [M2.act1/Assignment/0..4] | MODIFICATION in [M2.act1/Assignment/0..4] | ||
[[Category:Developer documentation]] | [[Category:Developer documentation]] |
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]