Difference between pages "D32 General Platform Maintenance" and "Event-B Classdiagrams"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Colin
 
Line 1: Line 1:
= Overview =
+
[[Image:IUMLB_big.png|frame|left]]
The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of Deploy, these bugs and features are reported either by mail or through dedicated SourceForge trackers.
+
{{TOCright}}
 +
==Introduction==
 +
In iUML-B, Class diagrams are used to define and visualize entity-relationship data models. They can be added to Event-B Machines and Event-B Contexts and visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it. The diagram defines type, sub-type and further constraint information for the data by generating invariants or axioms.
  
The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:
+
==Principles of Operation==
* Proof replay of undischarged POs (releases 1.3 and upper)
 
: It often happens, while modifying a model, that a set of previously manually discharged POs are slightly changed and need to be discharged again. However, replaying the proof for those POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request was expressed by [https://sourceforge.net/tracker/?func=detail&aid=2949606&group_id=108850&atid=651672 end users]. See [http://wiki.event-b.org/index.php/Proof_Obligation_Commands].
 
* Rule Details View (releases 2.0 and upper)
 
: When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more informations about the rules being involved in a proof, such as instantiation details, hidden hypotheses, etc. The [http://wiki.event-b.org/index.php/Rodin_Proving_Perspective#Rule_Details_View Rule Details View] displaying such details has been added.
 
* Refactoring plug-in (releases 1.2 and upper)
 
:
 
* Documentation
 
: Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated [http://wiki.event-b.org/index.php/Plug-in_Tutorial tutorial] has been written accordingly, and was the support of a training session given at the [http://www.event-b.org/rodin10.html Rodin User and Developer Workshop] in Düsseldorf this year.
 
  
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
+
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.  
  
= Motivations =
+
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).
The evolutive maintenance (resp. corrective maintenance) has its origin in the Deploy project's description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the Deploy project's birth, various streams can be used to express feature requests or track an encountered bug :
 
: - [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation dedicated trackers],
 
: - mail to the deploy user list, etc.
 
During the WP9 meetings, maintenance tasks to perform are being given a priority and are assigned to an according WP9 partner (as mentionned in the D23). The higher priority is given to WP partners requests.
 
  
The following table describes the performed and scheduled tasks motivating the evolutive maintenance :
+
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.
  
{{SimpleHeader}}
+
===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.
! scope=col | Type || Origin || Maintenance Task || Done || Scheduled
+
* '''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.
|Evolutive Maintenance || End Users|| Adding a replay proof command in the Event-B Explorer || ||
+
* '''Attributes''' are similar to  associations except that the target is given by a text string (the attribute type property).
|-   
 
|}
 
  
= Choices / Decisions =
+
===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.
 +
* 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.
  
---MAC plat 3.6
+
===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 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.
  
= Available Documentation =
+
===Secondary information===
As in the previous D23 delivrable, the following pages give useful information about the Rodin platform releases:
+
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.
* Release notes.
 
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].
 
: More details are provided in the notes distributed with each release (eg. [http://sourceforge.net/project/shownotes.php?release_id=693928]).
 
* Bugs.
 
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850].
 
* Feature requests.
 
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672].
 
  
= Planning =
+
==Examples==
The [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page lists in particular the upcoming releases and give the scheduled release dates.
+
For example when a class diagram is first drawn and has not been linked to data it looks like this:
  
[[Category:D32 Deliverable]]
+
[[File:Cd1_unlinked.png]]
 +
 
 +
 
 +
Generating this diagram produces no output to the Event-B.
 +
The diagram elements must first be linked to data using the '''Link Data''' or '''Create & Link''' buttons in the properties sheet.
 +
The followng screenshot shows the association being linked to a variable ''b'' that already exists in the machine.
 +
 
 +
[[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.
 +
 
 +
[[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 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]]
 +
 
 +
 
 +
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]]

Latest revision as of 05:07, 6 October 2015

IUMLB big.png

Introduction

In iUML-B, Class diagrams are used to define and visualize entity-relationship data models. They can be added to Event-B Machines and Event-B Contexts and visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it. The diagram defines type, sub-type and further constraint information for the data by generating 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 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.

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).

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

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.
  • 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).

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.
  • 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

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

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.

Examples

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

Cd1 unlinked.png


Generating this diagram produces no output to the Event-B. The diagram elements must first be linked to data using the Link Data or Create & Link buttons in the properties sheet. The followng screenshot shows the association being linked to a variable b that already exists in the machine.

LinkData.png


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.

CreatLink.png


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.

ClassDiagGen.png


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.

ClassDiagGen2.png