imported>Nicolas |
imported>WikiSysop |
Line 1: |
Line 1: |
− | ==Purpose== | + | == Event-B Language Documentation == |
| | | |
− | Event-B indexers populate the index repository. Currently, indexers are implemented for the following files : | + | [[Event-B Mathematical Language]] |
− | * machine (.bum)
| |
− | * context (.buc)
| |
| | | |
− | | + | [[Event-B Modelling Language]] |
− | ==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]]
| |