7.2 Class Attributes

The class attributes represent additional BML-entities added to a class

• Version - BML encoding format version number
• ClassModifiers - BML modifiers of the class
• GhostField - ghost fields
• ModelField - model fields
• ModelMethod - model methods
• ClassInvariant - class invariants
• Constraint - history constraints
• SecondConstantPool - pool of values used by BML related attributes

• The Version attribute
• The ClassModifiers attribute
• The GhostField attribute
• The ModelField attribute
• The ModelMethod attribute
• The ClassInvariant attribute
• The Constraint attribute
• The SecondConstantPool attribute