Viewpoint Lattices
From AtlanMod
Contents |
Model Subtyping
In [1], authors defines (following the work of [2]) a sub-typing relationship for KM3 environement. This relation is defined as (for metamodel) Ma ≤ Mb if the following conditions hold:
- Metamodel M' is a subtype of Metamodel M (M' ≤ M) iff:
∀K ∈ {M.Package} | ∃ K' ∈ {M.Package} | (K' ≤ K)
- Package K' is subtype of Package K (K' ≤ K) iff:
(K'.name = K.name) Λ ∀C ∈ {K.Class} | ∃ C' ∈ {K'.Class} | (C' ≤ C)
- Class C' is a subtype of Class C (C' ≤ C) iff:
(C'.name = C.name) Λ (C.isAbstract ≤ C'.isAbstract) Λ ∀ P ∈ {C.Attribute} | ∃ P' ∈ {C'.Attribute} | (P' ≤ P) Λ ∀ R ∈ {C.Reference} | ∃ R' ∈ {C'.Reference} | (R' ≤ R)
- Attribute P' is subtype of Attribute P (P' ≤ P) iff:
(P'.name = P.name) Λ (P'.type ≤ P.type) Λ (P'.multiplicity ≤ P.multiplicity) Λ (P'.isUnique ≤ P.isUnique) Λ (P'.isOrdered ≤ P.isOrdered)
- Reference R' is a subtype of Reference R (R' ≤ R) iff:
(R'.name = R.name) Λ (R'.type ≤ R.type) Λ (R'.multiplicity ≤ R.multiplicity) Λ (R'.isUnique ≤ R.isUnique) Λ (R'.isOrdered ≤ R.isOrdered) Λ (R'.isContainer ≤ R.isContainer) Λ (R.opposite ≠ null) ⇒ (R'.opposite ≠ null) Λ (R'.opposite ≤ R.opposite)
Subtype Relation : an order Relation
A relation is a (partial) order relation iff it is reflexive, antisymmetric and transitive.
In the following demonstration, we define M: a set of metamodels. We demonstrates the three properties against the definition of [1], written above. We need to demonstrate that for each elements of a metamodel (written in KM3) : Package, class, attribute and reference. The ≤ relation is based on comparison of several modeling features: names (String e.g. Class Name), cardinality and properties (boolean, e.g isAbstract). If we the ≤ relation validates all properties (eg. Reflexive, antisymmetric and transitive) on modeling element, ≤ is a partial order relation. Other cases, for example comparing the attributes of a class : ∀ P ∈ {C.Attribute} | ∃ P' ∈ {C'.Attribute} | (P' ≤ P) mean that P' is a sub-set of P.
- Sub-typing relation on Boolean a ≤ b ⇔ (b ⇒ a) :
Reflexivity : a ≤ a : for each value of a (false, true) a ⇒ a remains true. The relation ≤ is reflexive for boolean. Antisymmetry : (a ≤ b) and (b ≤ a) ⇔ (a ⇒ b) Λ (b ⇒ a) : in that case : a ⇔ b, for boolean a = b. The relation ≤ is Antisymmetric for boolean. Transitivity : (a ≤ b) Λ (b ≤ c) ⇔ (a ⇒ b) Λ(b ⇒ c) : due to the transitivity of ⇒ relation on boolean : (a ⇒ b) so a ≤ c is true. The relation ≤ is transitive for boolean.
- Sub-typing relation on cardinalities: [a'..b'] ≤ [a..b] ⇔ (a' ≤ a) Λ (b' ≥ b)
In the definition above, the ≤ relation between entities refeers to the mathematical operator between integer (plus additional *). Such operator is of course already an order operator. For Example: [0..*] ≤ [0..1] ≤ [1..1]. This order goes from the more "permissive cardinality" to the less permissive.
- Sub-typing relation on sets of modeling elements
Since we consider set of attributes or references the sub-typing relation act as a "sub-set" relation : ⊆. This relation is a well-know order relation.
Reflexivity (∀ a ∈ M, a ≤ a )
Antisymmetry (∀ a, b ∈ M : if a ≤ b and b ≤ a then a = b)
Transitivity (∀ a, b ∈ M : if a ≤ b and b &le c then a ≤ c)
Lattice of KM3 modeling elements
Bibliography
[1] Romero, J.R., Rivera, J.E., Duran, F., Vallecillo, A., Formal and Tool Support for Model Driven Engineering with Maude. Journal of Object Technology, vol 6., no. 9., 2007.
