Event-B Classdiagrams - Revision history

imported>Colin: /* Examples */

2015-10-06T05:07:29Z

Examples

← Older revision		Revision as of 05:07, 6 October 2015
Line 49:		Line 49:

	[[File:ClassDiagGen.png\|800px]]		[[File:ClassDiagGen.png\|800px]]


			In the following screenshot, B has been linked to a constant in the context X0. The supertype relation from B to A generates the axiom, B ∈ ℙ(A).
			A method (with a parameter, guard and action) and an invariant have been added to class A and their translations are shown in the machine m0.

			[[File:ClassDiagGen2.png\|800px]]

imported>Colin at 14:55, 5 October 2015

2015-10-05T14:55:22Z

← Older revision		Revision as of 14:55, 5 October 2015
Line 1:		Line 1:
	~~''this page is under construction''~~
	[[Image:IUMLB_big.png\|frame\|left]]		[[Image:IUMLB_big.png\|frame\|left]]
	{{TOCright}}		{{TOCright}}

imported>Colin: /* Other Elements of a Class Diagram */

2015-10-05T14:54:22Z

Other Elements of a Class Diagram

← Older revision		Revision as of 14:54, 5 October 2015
Line 20:		Line 20:

	===Other Elements of a Class Diagram===		===Other Elements of a Class Diagram===
	* Constraints can be added to classes. The constraint is automatically universally quantified for all instances of the class. The user is expected to use the class' ''self name'' to represent the quantifier local variable. (By default the self name is ''this_<className>'' but it can be altered in the properties of the class). The constraint will generate an axiom or an invariant depending on wheter the class diagram is owned by a context or machine.		* '''Constraints''' can be added to classes. The constraint is automatically universally quantified for all instances of the class. The user is expected to use the class' ''self name'' to represent the quantifier local variable. (By default the self name is ''this_<className>'' but it can be altered in the properties of the class). The constraint will generate an axiom or an invariant depending on wheter the class diagram is owned by a context or machine.
	* For class diagrams that are owned by a machine, methods may be placed in classes. Methods are linked to events of the machine and a parameter is generated to represent the contextual instance, using the class' self-name. The user is expected to use the self name in guards and actions of the method. Note that the method-event elaborates relationship is many to many. Hence several methods in different classes could elaborate the same event. Conversely the same method may contribute its behaviour to several different events.		* For class diagrams that are owned by a machine, '''methods''' may be placed in classes. Methods are linked to events of the machine and a parameter is generated to represent the contextual instance, using the class' self-name. The user is expected to use the self name in guards and actions of the method. Note that the method-event elaborates relationship is many to many. Hence several methods in different classes could elaborate the same event. Conversely the same method may contribute its behaviour to several different events.

	===Scope===		===Scope===

imported>Colin: /* Principles of Operation */

2015-10-05T14:54:00Z

Principles of Operation

← Older revision		Revision as of 14:54, 5 October 2015
Line 19:		Line 19:
	* '''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).		* '''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).

	===~~Elaboration and Generation~~===		===Other Elements of a Class Diagram===
	~~tbd~~		* Constraints can be added to classes. The constraint is automatically universally quantified for all instances of the class. The user is expected to use the class' ''self name'' to represent the quantifier local variable. (By default the self name is ''this_<className>'' but it can be altered in the properties of the class). The constraint will generate an axiom or an invariant depending on wheter the class diagram is owned by a context or machine.
			* For class diagrams that are owned by a machine, methods may be placed in classes. Methods are linked to events of the machine and a parameter is generated to represent the contextual instance, using the class' self-name. The user is expected to use the self name in guards and actions of the method. Note that the method-event elaborates relationship is many to many. Hence several methods in different classes could elaborate the same event. Conversely the same method may contribute its behaviour to several different events.

	===Scope===		===Scope===

imported>Colin: /* Examples */

2015-10-05T14:36:58Z

Examples

← Older revision		Revision as of 14:36, 5 October 2015
Line 32:		Line 32:

	[[File:Cd1_unlinked.png]]		[[File:Cd1_unlinked.png]]


	Generating this diagram produces no output to the Event-B.		Generating this diagram produces no output to the Event-B.
Line 38:		Line 39:

	[[File:LinkData.png\|800px]]		[[File:LinkData.png\|800px]]


	The following screenshot shows the class A being used to create and link to a carrier set in the seen context X0. Note that the carrier set is created in X0 immediately. It is not necessary to generate.		The following screenshot shows the class A being used to create and link to a carrier set in the seen context X0. Note that the carrier set is created in X0 immediately. It is not necessary to generate.
Line 43:		Line 45:
	[[File:CreatLink.png\|800px]]		[[File:CreatLink.png\|800px]]

	After linking these diagram elements they are automatically rendered differently including icons for variables (b) and sets (A). Generating at this stage introduces an invariant for the variable b to say that it is a relation between A and B. Since B only exists in the diagram~~, it~~ is not yet linked to any data, this causes an error in the machine. However, note that the invariant is still generated using the class name, B. in fact we could replace the class name with any valid expression (e.g. NAT) representing a set of instances.
			After linking these diagram elements they are automatically rendered differently including icons for variables (b) and sets (A). Generating at this stage introduces an invariant for the association variable b to say that it is a relation between A and B. Since B only exists in the diagram and is not yet linked to any data, this causes an error in the machine. However, note that the invariant is still generated using the class name, B. In fact we could replace the class name with any valid expression (e.g. NAT) representing a set of instances.

	[[File:ClassDiagGen.png\|800px]]		[[File:ClassDiagGen.png\|800px]]

imported>Colin: /* Main Data Elements of a Class Diagram */

2015-10-05T14:33:03Z

Main Data Elements of a Class Diagram

← Older revision		Revision as of 14:33, 5 October 2015
Line 15:		Line 15:
	===Main Data Elements of a Class Diagram===		===Main Data Elements of a Class Diagram===
	The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize Event-B data items (carrier sets, constants or variables) in the Event-B model. Only a class can visualize a carrier set. The class diagram also visualizes the relationships between these data items and generates constraints (invariants and axioms as appropriate) as follows.		The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize Event-B data items (carrier sets, constants or variables) in the Event-B model. Only a class can visualize a carrier set. The class diagram also visualizes the relationships between these data items and generates constraints (invariants and axioms as appropriate) as follows.
	'''Class Supertype''' relationships between classes represent that the source is a sub-set of the target superset.		* '''Class Supertype''' relationships between classes represent that the source is a sub-set of the target superset.
	'''Association''' relationships represent that the association data is a relation between instances of the source and target classes. Cardinality may be used to further constrain the relationship to be for example a function, injection or surjection.		* '''Association''' relationships represent that the association data is a relation between instances of the source and target classes. Cardinality may be used to further constrain the relationship to be for example a function, injection or surjection.
	'''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).		* '''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).

	===Elaboration and Generation===		===Elaboration and Generation===

imported>Colin: /* Main Data Elements of a Class Diagram */

2015-10-05T14:30:45Z

Main Data Elements of a Class Diagram

← Older revision		Revision as of 14:30, 5 October 2015
Line 14:		Line 14:

	===Main Data Elements of a Class Diagram===		===Main Data Elements of a Class Diagram===
	The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize an Event-B data ~~item~~ (~~set constant~~ or ~~variable~~) in the Event-B model. Only a class can visualize a set. The class diagram also visualizes the ~~type~~ and ~~subtype of the data item~~ as follows.		The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize Event-B data items (carrier sets, constants or variables) in the Event-B model. Only a class can visualize a carrier set. The class diagram also visualizes the relationships between these data items and generates constraints (invariants and axioms as appropriate) as follows.
	~~====~~Class~~====~~		'''Class Supertype''' relationships between classes represent that the source is a sub-set of the target superset.
	~~A Class visualizes a data item~~ that is a set ~~or subset~~.		'''Association''' relationships represent that the association data is a relation between instances of the source and target classes. Cardinality may be used to further constrain the relationship to be for example a function, injection or surjection.
	~~a) If~~ the ~~class diagram~~ is in a ~~Context~~ and the ~~class has no generalization relationships~~, ~~and its~~		'''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).
	~~====Association====~~
	~~====Atttribute====~~

	===Elaboration and Generation===		===Elaboration and Generation===

imported>Colin: /* Principles of Operation */

2015-10-05T14:02:48Z

Principles of Operation

← Older revision		Revision as of 14:02, 5 October 2015
Line 7:		Line 7:
	==Principles of Operation==		==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 diagram element elaborates properties of the data item.		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 diagram element elaborates properties of the data item. Any data element within scope, locally within 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.

	Any data element within scope, locally within 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 sets are within scope to link to and methods cannot be used in classes).		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 sets are within scope to link to and methods cannot be used in classes).

imported>Colin at 14:01, 5 October 2015

2015-10-05T14:01:55Z

← Older revision		Revision as of 14:01, 5 October 2015
Line 15:		Line 15:
	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 paramter representing the class instance (similar to 'this' or 'self' in programming languages). When in variable classes (i.e. a class that elaborates a variable) methods may be constructors or destructors.		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 paramter representing the class instance (similar to 'this' or 'self' in programming languages). 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==		===Main Data Elements of a Class Diagram===
	The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize an Event-B data item (set constant or variable) in the Event-B model. Only a class can visualize a set. The class diagram also visualizes the type and subtype of the data item as follows.		The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize an Event-B data item (set constant or variable) in the Event-B model. Only a class can visualize a set. The class diagram also visualizes the type and subtype of the data item as follows.
	===Class===		====Class====
	A Class visualizes a data item that is a set or subset.		A Class 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		a) If the class diagram is in a Context and the class has no generalization relationships, and its
	===Association===		====Association====
	===Atttribute===		====Atttribute====

	==Elaboration and Generation==		===Elaboration and Generation===
	tbd		tbd

	==Scope==		===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.		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 visualize sets and constants in the containing context and visualize sets and constants in any context which is (transitively) extended by the containing context. A class diagram in a machine may define/visualize variables in the containing machine, visualize variables in any machine it (transitively) refines and visualize sets and constants in any context that is seen by the machine or any Context that is (transitively) extended by a context that is seen by the machine.

	==Secondary information==		===Secondary information===
	Colour is used to indicate whether a diagram element has been linked to data. Icons are used to indicate the kind (set, constant or variable) of elaborated data.		Colour is used to indicate whether a diagram element has been linked to data. Icons are used to indicate the kind (set, constant or variable) of elaborated data.

	==~~Example~~==		==Examples==
	For example when a class diagram is first drawn and has not been linked to data it looks like this:		For example when a class diagram is first drawn and has not been linked to data it looks like this:

Line 50:		Line 50:

	[[File:ClassDiagGen.png\|800px]]		[[File:ClassDiagGen.png\|800px]]

	~~==Class Diagrams in Contexts==~~
	~~subtype~~

	~~==Class Diagrams in Machines==~~

imported>Colin: /* Example */

2015-10-05T13:58:12Z

Example

← Older revision		Revision as of 13:58, 5 October 2015
Line 46:		Line 46:

	[[File:CreatLink.png\|800px]]		[[File:CreatLink.png\|800px]]

			After linking these diagram elements they are automatically rendered differently including icons for variables (b) and sets (A). Generating at this stage introduces an invariant for the variable b to say that it is a relation between A and B. Since B only exists in the diagram, it is not yet linked to any data, this causes an error in the machine. However, note that the invariant is still generated using the class name, B. in fact we could replace the class name with any valid expression (e.g. NAT) representing a set of instances.

			[[File:ClassDiagGen.png\|800px]]

	==Class Diagrams in Contexts==		==Class Diagrams in Contexts==