Rodin Handbook





 

3.2.8 Visibility of identifiers

Expressions and predicates are comprised of certain Event-B elements. The following table describes the elements that each predicate or expression use:

 

sets

constants

variables

parameters

     

concrete

abstract

concrete

abstract

axiom

$\times $

$\times $

       

invariant

$\times $

$\times $

$\times $

$\times $

   

variant

$\times $

$\times $

$\times $

$\times $

   

guard

$\times $

$\times $

$\times $

 

$\times $

 

witness$^{*}$

$\times $

$\times $

$\times $

$\times $

$\times $

$\times $

action$^{*}$

$\times $

$\times $

$\times $

 

$\times $

 

However, expressions and predicates can only use elements that are identified within a specific scope:

Sets

Sets can be used when they are defined in the context (in case of an axiom) or in a seen context. If a context extends another context, the sets of the extended context are treated as if they are defined in the extending context.

Constants

Constants can be used when they are defined in the context (in the case of an axiom) or in a seen context.

Concrete Variables

Concrete variables that are defined in the machine itself can be used.

Abstract Variables

Abstract variables that are defined in an abstract machine can be used.

Concrete Parameters

Parameters that are defined in the event itself can be used.

Abstract Parameters

Parameters that are defined in an abstract event can be used.

$\mbox{}^{*}$ Witnesses and actions have additional elements in their scope. Section 3.2.4.4.4 provides more information about witnesses, and Section 3.3.8 explains the scope for actions that have different types of assignments in further detail.