Class Diagram

Return to UML-B

Class diagrams are used to describe the behavioural part of a model. Classes represent subsets (variable or fixed) of the ClassTypes that were introduced in the context. The class’ associations and attributes are similar to those in the context but represent variables instead of constants. The correspondence between an association’s multiplicity constraints and the constraints on the resulting Event-B relationship is clear from the drawing tool. The multiplicity properties are described in the properties view using the usual mathematical terminology (functional, total, injective, surjective) with the UML style multiplicity also shown and annotated automatically on the diagram.

Classes may contain events that modify their attributes. Event parameters can be added to an event providing local variables to be used in the transition’s guards and actions. These parameters can be used to model inputs and outputs. Class events implicitly utilise a parameter to non-deterministically select the affected instance of the class. This instance is referred to via the reserved word self when referencing the attributes of the class.