imported>Nicolas |
|
| Line 1: |
Line 1: |
| − | ==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 ({{class|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 ({{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.var1/Identifier]
| |
| − | 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.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]
| |
| − |
| |
| − | [[Category:Developer documentation]]
| |
