|
| |||||
12.6 UML Class Diagram Supported Features |
In the following sections we present by examples all those UML class diagrams features that can be translated to RSL with the UML2RSL tool.
In the simplest case, a class just consists of a name. It also can have a set of attributes, a set of operations and a multiplicity.
Each attribute must have a name, an optional type, a multiplicity, a scope ({classifier} or {instance}), and a changeability ({frozen}, {addOnly} or {changeable}). The default for the scope is {instance}, for the changeability is {changeable}, and for the multiplicity is 1..1.
An operation must have a name and can have a list of formal parameters, where each parameter must have a name and an optional type. Furthermore, an operation has an optional result-type, a scope and it can be abstract.
The default for the multiplicity of a class is *..*.
For example, let us consider the simple class diagram in figure 12.6.1 which consists only of the class Window whose multiplicity is *..* (by default). It has 5 attributes and 2 operations:
title, which is a frozen attribute with multiplicity 1..* and {instance} scope;
default_size and max_size that are changeable attributes with multiplicity 1..1 and {classifier} scope;
size and visible are attributes whose changeabilities are {changeable}, their multiplicities are 1..*, and their scopes are {instance}.
number_of_windows is an operation whose scope is {classifier}; it has no parameters and its result type is Int.
show is an operation whose scope is {instance}; it has no parameters and its result type is not given.
The resulting specification will consist of four RSL modules: S, WINDOWS_, WINDOW and TYPES. The module S uses the module WINDOWS_, which uses WINDOW_, and WINDOW_ uses in turn TYPES.The module WINDOW_ has the specification for an object of the class Window.
TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object WINDOW_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
size : Window → Size, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
default_size : Window → Size, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
max_size : Window → Size, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
visible : Window → boolean, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
title : Window → Char-set, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_size : Size × Window -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_size(at, o) as o′ post size(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_size(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_size : Size × Window → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_default_size : Size × Window -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_default_size(at, o) as o′ post | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
default_size(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_default_size(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_default_size : Size × Window → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_max_size : Size × Window -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_max_size(at, o) as o′ post max_size(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_max_size(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_max_size : Size × Window → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_visible : boolean × Window -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_visible(at, o) as o′ post visible(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_visible(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_visible : boolean × Window → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
show : Window → Window, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent : Window → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(o) ≡ card title(o) ≥ 1 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
The RSL abstract type Window is generated to specify the class sort. It denotes the set of all possible class instances or objects.
For each attribute, the tool generates an observer on the class sort. Each one of these observers takes an instance of the class and returns a value belonging to the corresponding attribute type.
The operations are specified as RSL functions, which have their domain in the Cartesian product of the class sort and the corresponding operation parameters. Their ranges correspond to the operation result types. When an operation in the class diagram does not return a value, it means that the operation performs some behaviour -- based on the class structure and its parameters -- which possibly changes the class structure. Therefore, in this situation, the RSL function will return the class sort. For example, the operation show in figure 12.6.1. However, when the scope of an operation is the class, since the operation acts on the class container, we do not generate the corresponding function on an instance of the class, but on the type defined for the class container. Therefore, the value used to specify the operation is generated in the module that holds the specification of the class. As we can see in the example,number_of_windows is placed in the module WINDOWS_.
In a class, besides the typical operation intended to return the value of an attribute, it is common to have an operation to modify the attribute, and since, frequently, the update of a given attribute occurs under a given pre-condition, RSL functions are generated for this purpose. Their pre-conditions should be completed by the user. If they are not necessary, then they may be removed. In the example above, the functions update_size, preupdate_size, update_default_size, preupdate_default_size, update_max_size, preupdate_max_size, update_visible and preupdate_visible were generated for this purpose. The corresponding update and preupdate functions for the attribute title were not generated because title is a frozen attribute.
The module WINDOWS_ has the specification for the class Window.
WINDOW_ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object WINDOWS_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Window = WINDOW_.Window, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Windows = Window_Id -m-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
empty : Windows = [], | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
add : Window_Id × Window × Windows -~-> Windows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
add(id, o, c) ≡ c † [id ↦ o] pre ~ is_in(id, c), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
del : Window_Id × Windows -~-> Windows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
del(id, c) ≡ c \ {id} pre is_in(id, c), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
is_in : Window_Id × Windows → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
is_in(id, c) ≡ id ∈ dom c, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
get : Window_Id × Windows -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
get(id, c) ≡ c(id) pre is_in(id, c), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update : Window_Id × Window × Windows -~-> Windows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update(id, o, c) ≡ c † [id ↦ o] pre is_in(id, c), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
number_of_windows : Windows → Int, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent : Windows → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(c) ≡ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id ∈ dom c ⇒ WINDOW_.consistent(c(id))) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id1, id2 : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom c /\ id2 ∈ dom c) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.default_size(c(id1)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.default_size(c(id2))) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id1, id2 : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom c /\ id2 ∈ dom c) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.max_size(c(id1)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.max_size(c(id2))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
The type Windows describes the set of all the possible observable states in which the class Window can be, that is, a set of sets of Window objects or, in other words, all the possible sets of objects that can be observed at a given moment. We refer to it as the class container type. A characteristic of the objects is that each object is distinguishable from the other objects of the class, even if they have exactly the same property values. Consequently, the class container type is defined as a map from a set of object identifiers to the Window class sort.
For each class in the class diagram, new objects can be created and existing objects can be destroyed or modified. Therefore, some typical functions that operate on the set of instances of each class are generated by the translator. They are empty, add, del, is_in, get, and update.
When the scope of an operation is the class, since the operation acts on the class container, the RSL value used to specify the operation is placed in the module that holds the specification of the class. As we said before, number_of_windows is a class scoped operation, therefore its definition is generated in the module WINDOWS_.
The resulting RSL code produced for module S is given below.
WINDOWS_ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object S : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Sys :: windows : WINDOWS_.Windows ↔ replace_windows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_windows : WINDOWS_.Windows × Sys -~-> Sys | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_windows(c, s) ≡ replace_windows(c, s) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_windows(c, s), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_windows : WINDOWS_.Windows × Sys → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
number_of_windows_in_Windows : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOWS_.Windows × Sys → Int, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
show_in_Window : WINDOW_.Window × Sys → Sys, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent : Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(s) ≡ WINDOWS_.consistent(windows(s)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
axiom | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
∀ s : Sys, c : WINDOWS_.Windows • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_windows(c, s) as s′ post | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(s′) /\ frozenAtts_in_Window(s′, s) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre consistent(s) /\ preupdate_windows(c, s) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
frozenAtts_in_Window : Sys × Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
frozenAtts_in_Window(s′, s) ≡ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id ∈ dom windows(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id ∈ dom windows(s′)) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.title(windows(s)(id)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.title(windows(s′)(id))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
Each class in the class diagram has its corresponding field in the RSL record Sys to hold its class container. The type Sys describes all the possible instances of the system being modeled by the class diagram. In our example there is just one such field, whose name is windows that corresponds to the class container for the class Window.
The function update_windows is an extra operation defined to produce changes on the class container and preupdate_windows is the function signature for its pre-condition. The preupdate_windows definition will have to be completed later by the developer, according to his needs.
Since we are interested only in consistent systems, it is necessary to express consistency. This is achieved by a collection of axioms expressing the property that all the top-level state-changing functions maintain the system in a consistent state. In our example the only top-level state-changing function we have is update_windows, therefore there is an axiom for it. We capture all the model invariants in a boolean function named consistent which is defined as the conjunction among all the necessary predicates to express all the model constraints.
Class diagrams as well as their composing elements may have different constraints associated with them. As we want to check consistency on the whole system, that is, to check that all the constraints hold, we define a series of axioms on the top level module in order to check that the system is in a consistent state before and after any state change occurs. For this reason, not only the function consistent in the top-level module S is generated but a series of boolean functions are generated in the lower level modules as well. Inside each module that has been defined either to specify an object or a class, we define one of these boolean functions -- that we also name consistent. They allow one to check the consistency of one object and the consistency of all the instances of the class, respectively. The last ones make use of the lower level ones, that is those defined for one instance of the class. The function consistent in the top level module is generated to check the consistency of the whole class diagram, and it uses -- in turn -- all the lower level functions consistent defined for each one of the classes, guaranteeing in this way the consistency of the whole system.
In which of the several consistent functions the predicate for expressing a given property is put depends on what kind of restriction we are checking and for which element we want to check it. In our example, we have a predicate in the function consistent of the module WINDOW_ to check the multiplicity of the attribute title.
consistent : Window → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(o) ≡ card title(o) ≥ 1 |
In the function consistent of module WINDOWS_ we find the conjunction of three predicates.
consistent : Windows → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(c) ≡ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id ∈ dom c ⇒ WINDOW_.consistent(c(id))) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id1, id2 : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom c /\ id2 ∈ dom c) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.default_size(c(id1)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.default_size(c(id2))) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id1, id2 : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom c /\ id2 ∈ dom c) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.max_size(c(id1)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.max_size(c(id2))) |
The first one checks the consistency of all the objects in the class container, making use of the lower level function consistent of module WINDOW_. The second and third ones were generated to express the fact that default_size and max_size are class scoped attributes. Since the multiplicity of the class is *..* no predicate must be generated. Other class multiplicities generate constraints (see section Multiplicities in [9]).
Finally, in the top-level module S of the example, we found a predicate to check the consistency of the whole system. In this example, it reduces to check only the consistency of the Window class container making use of the function consistent of lower level module WINDOWS_.
consistent : Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(s) ≡ WINDOWS_.consistent(windows(s)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
axiom | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
∀ s : Sys, c : WINDOWS_.Windows • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_windows(c, s) as s′ post | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(s′) /\ frozenAtts_in_Window(s′, s) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre consistent(s) /\ preupdate_windows(c, s) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
frozenAtts_in_Window : Sys × Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
frozenAtts_in_Window(s′, s) ≡ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id : Window_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id ∈ dom windows(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id ∈ dom windows(s′)) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.title(windows(s)(id)) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
WINDOW_.title(windows(s′)(id))) |
Note that since it is necessary to check the property {frozen} for the window attribute title, a predicate is generated in the post-condition of the axiom corresponding to the class Window. It states for each object of class Window that the value of the attribute title remains unchanged after the system state has changed.
Finally, we have the module TYPES that constains the definitions of all the abstract types found in the model. The standard types boolean, char and double found in the class diagram are defined in TYPES as Bool, Char and Real RSL types respectively. The type Window_Id is used for the object identifiers in the class container of Window.
object TYPES : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Size, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
boolean = Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Window_Id | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
Each association end must have at least a name and can have several adornments: a given multiplicity, a given navigability, it can be composite or aggregate and -- like attributes -- it can have a changeabilty. The default for association multiplicity is 1..1, for the navigability is false, and for the changeability is {changeable}.
An association is translated as two RSL functions among the involved classes (or one depending on its navigability ends, as we will see next). A function is generated for each of the involved class and it returns the remaining related object.
For example, for the association has_copies shown in figure 12.6.2 two observers will be generated: one in class Item to retrieve all the existing copies for a given item, and another in class Copy to obtain the corresponding item for a given copy. The tool will also generate all the functions for updating the objects retrieved by the association.TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object ITEM_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type Item | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
title : Item → title, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
. . . | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
has_copies : Item → Copy_Id-set, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_has_copies : Copy_Id-set × Item -~-> Item | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_has_copies(a, o) as o′ post has_copies(o′) = a | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_has_copies(a, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_has_copies : Copy_Id-set × Item → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
. . . | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object COPY_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type Copy | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
status : Copy → status, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
has_copies : Copy → Item_Id, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_has_copies : Item_Id × Copy -~-> Copy | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_has_copies(a, o) as o′ post has_copies(o′) = a | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_has_copies(a, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_has_copies : Item_Id × Copy → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
Note that in the case of the class Item, the returned types for has_copies is a set of object identifiers of class Copy, while the has_copies of Copy only returns an object identifier of class Item. This structural distinction is because the multiplicities at the association ends are different. Association multiplicities are treated in detail in the section Multiplicities in [9].
When the association is navigable only in one direction, the tool will generate only one observer. For example, let us suppose that the association has_copies is navigable only from Item to Copy. In this case, only the function corresponding to the module ITEM_ will be generated. Association Navigation is treated deeply in the section Association Navigation in [9].
Since the observers generated for the associations return object identifier(s), a predicate for checking that such object identifiers actually exist in the class containers is generated. When the association is bidirectional, besides checking existence as before, it is also necessary to check bi-navigation. Since this kind of checking involves references to the containers of the navigable classes, they must be placed in a module that has access to all the containers, that is the top level module. Therefore, in the function consistent of the top level module the following predicates will be generated for association has_copies.
(∀ id1 : Item_Id, id2 : Copy_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom items(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id2 ∈ ITEM_.has_copies(items(s)(id1))) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id2 ∈ copys(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id1 = COPY_.has_copies(copys(s)(id2)))) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id1 : Copy_Id, id2 : Item_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id1 ∈ dom copys(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id2 = COPY_.has_copies(copys(s)(id1))) ⇒ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(id2 ∈ items(s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id1 ∈ ITEM_.has_copies(items(s)(id2)))) |
Such predicates for checking existence and bi-navigation take slightly different forms depending on the association end multiplicities. They are treated in detail in [9], section Existence and Bi-navigation constraints.
In this example, the changeability of the association ends is {changeable}, however the tool also translates {addonly} and {frozen} changeabilities. They are tretaed in the section Attribute and Association End Properties in [9].
Composition is a form of aggregation with coincident lifetime of the parts with the whole, i.e. the parts may be created after the whole, and can also be explicitly removed before the whole. However, if the whole is destroyed they die with it. Because of that, the multiplicity of a composite end -- unlike an aggregate end -- must be always at most one (it cannot be shared by different instances of the owner class). This is checked by the tool.
In figure 12.6.2 an example of a composition between the classes Company and Department and a recursive composition on Department are shown.
Structurally, a composition is equivalent to a general association. However, when we formalize the dynamic aspects of a composition, we make a distinction between a general association and a composition based on the property of coincident lifetimes of the whole and the parts. We express this property by means of a post-condition in the remove function of the whole. It assures that always when a whole is deleted all the parts that are currently associated are also deleted.Given the composition has between the part Department and the whole Company shown in figure 12.6.2, the coincident lifetime property is generated by the tool as follows:
del_Company : Company_Id × Sys -~-> Sys | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
del_Company(id, s) as s post | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∃ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
s′ : Sys, new_whole : COMPANYS_.Companys, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_parts : DEPARTMENTS_.Departments, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
parts : Department_Id-set | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
• | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
parts = COMPANY_.has(companys(s)(id)) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_parts = departments(s) \ parts /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
s′ = update_departments(new_parts, s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_whole = COMPANYS_.del(id, companys(s′)) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
s = update_companys(new_whole, s)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre can_del_Company(id, s), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
can_del_Company : Company_Id × Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
can_del_Company(id, s) ≡ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
COMPANYS_.is_in(id, companys(s)) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∃ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
s′ : Sys, new_whole : COMPANYS_.Companys, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_parts : DEPARTMENTS_.Departments, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
parts : Department_Id-set | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
• | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
parts = COMPANY_.has(companys(s)(id)) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_parts = departments(s) \ parts /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_departments(new_parts, s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
s′ = update_departments(new_parts, s) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
new_whole = COMPANYS_.del(id, companys(s′)) /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_companys(new_whole, s)), |
Note that in UML, when the type of an attribute corresponds to a class sort, this attribute is, in effect, a composition relationship between the class and the class of the attribute, or, in other words, the attribute is a shorthand for composition. Consequently, this kind of attribute is translated in the same way as a composition relationship which is navigable only from the whole to the parts.
Figure 12.6.2 shows an example of generalization between the classes Person and User.
The type that denotes the set of all the instances of the subclass is generated as an RSL subtype of the class sort that corresponds to the superclass (User in the example). New attributes and operations added to the subclass are translated as functions on the subclass type (level in the example).PERSON_ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object USER_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Person = PERSON_.Person, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
User = {| o : Person • is_a_User(o) |} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
level : User → level, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_level : level × User -~-> User | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_level(at, o) as o′ post level(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_level(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_level : level × User → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
is_a_User : Person → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent : User → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(o) ≡ PERSON_.consistent(o) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
The type corresponding to the type container of the subclass is generated as a subtype of the type used to specify the class container of the superclass, and the functions to operate on the class container are defined as usual.
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Users = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
{| super : PERSONS.Persons • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
(∀ id : Person_Id • | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id ∈ dom super ⇒ USER.is_a_User(super(id))) |} |
Figure 12.6.2 shows the dependency graph among the modules that have the specification for the superclass Person and the subclass User.
UML2RSL supports also the translation of abstract, root, leaf and template classes. We treat each below.
TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object WINDOW_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Window :: | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
size : Size ↔ replace_size | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
default_size : Size ↔ replace_default_size | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
max_size : Size ↔ replace_max_size | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
visible : boolean ↔ replace_visible | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
title : Char-set | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_size : Size × Window -~-> Window | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_size(at, o) ≡ replace_size(at, o) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_size(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_size : Size × Window → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
Note that the reconstructor for title is not generated because it is a frozen attribute.
Whenever an abstract class is translated, since objects cannot be created, the functions that operate on the class container are not generated. Furthermore, a constraint to assure that no instances of the abstract class have been created is generated on the type Sys.
Let us consider the example in figure 12.6.3. The RSL code for this constraint, which is generated in the function consistent of module S is shown below.consistent : Sys → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(s) ≡ ... /\ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
dom graphicobjects(s) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
dom circles(s) ∪ dom rectangles(s) |
It means that all the instances that can be in the class container corresponds to one of the concrete subclasses of the abstract class. This property can be expressed as the equality between the union of the abstract subclass containers and the abstract class container.
Abstract classes are classes that have at least one abstract operation. It means that the operation is incomplete and cannot be used, therefore an implementation must be given by a subclass. In RSL, the semantics of an abstract operation is given by hiding the operation name outside the module. So, outside the class module only references to the implementations given in the subclasses can occur. In the previous example, operation draw is abstract. To avoid the use of draw we hide its name.
TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object GRAPHICOBJECT_ : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
hide draw in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type GraphicObject | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
x : GraphicObject → Int, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
y : GraphicObject → Int, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
draw : GraphicObject → GraphicObject, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
A template class is translated to RSL in the same way as a concrete class but using a parameterized RSL scheme whose parameters corresponds to the class' parameters. In RSL when in a parameter expression only the name is given (as Element), it is assumed to be a type expression that resolves to a valid data type (for example, Person or Int). Otherwise, it must resolve to a valid value expression (like 3 or 24 for Int).
TYPES | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
scheme ARRAY__( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FPAR : | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type Element | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
k : Int | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end) = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type Array, Elements = FPAR.Element-set | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
elements : Array → Elements, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_elements : Elements × Array -~-> Array | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
update_elements(at, o) as o′ post elements(o′) = at | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
pre preupdate_elements(at, o), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
preupdate_elements : Elements × Array → Bool, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
apply : Int × Array → FPAR.Element, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
assign : FPAR.Element × Int × Array → Array, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent : Array → Bool | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
consistent(o) ≡ card elements(o) = FPAR.k | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end |
Since a template class cannot be used directly but only through its instantiations, the specification for its class container is not generated. However, for each instantiated class in the class diagram, UML2RSL generates the specification for its class container because they may have instances. These are generated as usual.
The semantics in RSL for the instantiation of a parameterized class is given by the instantiation of the corresponding parameterized scheme with its corresponding types and values. So, UML2RSL generates a new module to instantiate the array of 3 integers by instantiating the parameterized scheme ARRAY__ with Element equal to Int and k equal to 3 as follows:
ARRAY__ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
scheme ARRINT__ = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with TYPES in extend | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
APAR_ArrInt: | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
type | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Element = Int | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
value | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
k: Int = 3 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
with extend ARRAY__(APAR_ArrInt) with class type ArrInt=Array end |
and -- as usual -- UML2RSL generates an RSL object to represent the model corresponding to the specification of one object of class (ArrInt in this example).
ARRINT__ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
object ARRINT_: ARRINT__ |
As we can see, when we use template classes, the general structure of the resulting specification is sligthly different. In figure 12.6.3 we can see the RSL module dependency graph for the example of figure 12.6.3.
A more complete description of template class translation can be found in the section Parameterized Classes in [9].Some standard UML data types are made equivalent to the corresponding RSL types (by means of abbreviation definitions in TYPES.rsl) and so can be freely used in UML classes: see table 12.6.4 below.
The UML data type int is not accepted by the translator because it clashes with the RSL built-in function int.It is also possible to use the RSL built-in types Unit,
Bool, Int, Nat, Real, Char, and Text in
UML class diagrams. You will need to add them as new
Data Types
in the tool.
12.6 UML Class Diagram Supported Features | ||||||
|
|