Event-B Classdiagrams

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

Distinction between define and visualize (using the elaborates property) If the class diagram element elaborates a pre-existing data item (i.e. one that has not been generated by the class diagram generator) it is a visualization of existing Event-B and no new item is generated. If the class diagram element does not elaborate any Event-B data item, it is a definition of an Event-B data item. A new Event-B data item will be generated when the generator is invoked. The generated item will be deleted and re-generated when the generator is invoked. For defining data items, the elaborates property is left null and will be automatically set to the generated data item after generation. (n.b. there is a problem with this as need to identify that it is generated by this diagram element)

Alternatively the elaborates property can be set manually, using the Connect to existing data element button, to an existing data element (that is in scope and has not been generated). If the class diagram element elaborates a previously generated Event-B data item, it is a visualisation of that Event-B data item. The generated item will NOT be deleted and re-generated when the generator is invoked. An elaboration property can be removed and reset to null using the disconnect/delete generated element button. If the elaborated Event-B data item was generated by the class diagram generator, it is also deleted.

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