Event-B Classdiagrams

this page is under construction

Introduction

In iUML-B, Class diagrams are used to define and visualize data. They can be added to Event-B Machines and Event-B Contexts and define/visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it or generate (and subsequently elaborate) new data in order to define it. As well as defining/visualizing the actual data item, the arrangement of the diagram defines/visualizes type (and sub-type ) information for the data by elaborating invariants or axioms.

Principles of Operation

Classes, Attributes and Associations are all model elements that represent data. They can be linked to existing Event-B data elements: Variables, Constants or (for Classes only) Carrier Sets. This relationship is called Elaborates because the diagraam element elaborates properties of the data item.

Any data element within scope, locally wihtin the same machine or context, or via sees and extends, can be elaborated. As a short cut, a button is provided to create a new data item and link to it in one step.

Class diagrams can be added to Machines or Contexts, but note that some features are not available when in a Context (e.g. only constants and variables are within scope to link to and methods cannot be used in classes).

Methods can be placed inside Classes and link (elaborate) one or more events in the containing Machine. This means that the elaborated events are given a paraamter representing the class instance. When in variable classes (i.e. a class that elaborates a variable) methods may be constructors or destructors

Main Data Elements of a Class Diagram

The main data elements of a class diagram are class, association and attribute. These elements all define/visualize an Event-B data item (set constant or variable) in the Event-B model. Only a class can define/visualize a set. The class diagram also defines/visualizes the type and subtype of the data item as follows.

Class

A Class defines/visualizes a data item that is a set or subset. a) If the class diagram is in a Context and the class has no generalization relationships, and its

Elaboration and Generation

tbd

Scope

Elements of the class diagram can define data in the containing Event-B component and can visualize data in any Event-B component that is visible to the containing Event-B component (including itself). Hence a class diagram in a context may define/visualize sets and constants in the containing context and visualize sets and constants in any context which is extended (closure) by the containing context. A class diagram in a machine may define/visualize variables in the containing machine, visualize variables in any machine it refines (closure) and visualize sets and constants in any context that is seen by the machine or any Context that is extended by a context that is seen by the machine.

Secondary information

Colour is used to indicate whether the elaborated data has been generated or not and to indicate refinement/extension Icons are used to indicate the kind (set, constant or variable) of elaborated data.

Class Diagrams in Contexts

subtype