=Paper=
{{Paper
|id=Vol-1454/ramics15-st_33-42
|storemode=property
|title=Monoid Modules and Structured Document Algebra
|pdfUrl=https://ceur-ws.org/Vol-1454/ramics15-st_33-42.pdf
|volume=Vol-1454
}}
==Monoid Modules and Structured Document Algebra==
https://ceur-ws.org/Vol-1454/ramics15-st_33-42.pdf
Monoid Modules and Structured Document Algebra
(Extendend Abstract)
Andreas Zelend
Institut für Informatik, Universität Augsburg, Germany
zelend@informatik.uni-augsburg.de
1 Introduction
Feature Oriented Software Development (e.g. [3]) has been established in computer
science as a general programming paradigm that provides formalisms, meth-
ods, languages, and tools for building maintainable, customisable, and exten-
sible software product lines (SPLs) [8]. An SPL is a collection of programs that
share a common part, e.g., functionality or code fragments. To encode an SPL,
one can use variation points (VPs) in the source code. A VP is a location in a pro-
gram whose content, called a fragment, can vary among different members of
the SPL. In [2] a Structured Document Algebra (SDA) is used to algebraically de-
scribe modules that include VPs and their composition. In [4] we showed that
we can reason about SDA in a more general way using a so called relational pre-
domain monoid module (RMM). In this paper we present the following extensions
and results: an investigation of the structure of transformations, e.g., a condi-
tion when transformations commute, insights into the pre-order of modules,
and new properties of predomain monoid modules.
2 Structured Document Algebra
VPs and Fragments. Let V denote a set of VPs at which fragments may be in-
serted and F(V) be the set of fragments which may, among other things, contain
VPs from V. Elements of F(V) are denoted by f1 , f2 , . . . . There are two special
elements, a default fragment 0 and an error . An error signals an attempt to
assign two or more non-default fragments to the same VP within one module.
The addition, or supremum operator + on fragments obeys the following rules:
0+x=x, +x= ,
x+x=x, fi + fj = (i 6= j) ,
where x ∈ {0, fi , }. This structure forms a flat lattice with least element 0 and
greatest element and pairwise incomparable fi . By standard lattice theory +
is commutative, associative and idempotent and has 0 as its neutral element.
Modules. A module is a partial function m : V F(V). A VP v is assigned in m if
v ∈ dom(m), otherwise unassigned or external. By using partial functions rather
34 A. Zelend
than relations, a VP can be filled with at most one fragment (uniqueness). The
simplest module is the empty module 0, i.e., the empty partial map.
Module Addition. The main goal of feature oriented programming is to con-
struct programs step by step from reusable modules. In the algebra this is done
by module addition (+). Addition fuses two modules while maintaining unique-
ness (and signaling an error upon a conflict). Desirable properties for + are
commutativity and associativity. For module addition, + on fragments is lifted
to partial functions:
m(v) if v ∈ dom(m) − dom(n) ,
n(v) if v ∈ dom(n) − dom(m) ,
(m + n)(v) =df
m(v) + n(v) if v ∈ dom(m) ∩ dom(n) ,
undefined if v 6∈ dom(m) ∪ dom(n) .
If in the third case m(v) 6= n(v) and m(v), n(v) 6= 0 then (m + n)(v) = , thus
signalling an error.
The set of modules forms a commutative monoid under + with the neutral
element 0.
Deletion and Subtraction. For modules m and n the subtraction m − n is defined
as
m(v) if v ∈ dom(m) − dom(n) ,
(m − n)(v) =df
undefined otherwise.
Overriding. To allow overriding, an operation −. can be defined in terms of
subtraction and addition. Module m overrides n, written m −. n, if
m −. n = m + (n − m)
This replaces all assignments in n for which m also provides a value. −. is asso-
ciative and idempotent with neutral element 0.
Modules m and n are called compatible, in signs m ↓ n, if their fragments
coincide on their shared domains, i.e.,
m ↓ n ⇔df ∀ v ∈ dom(m) ∩ dom(n) : m(v) = n(v) .
We have chosen this characterization of compatibility with regard to the non-
relational abstract approach, to be pursued in Section 3, which especially needs
no converse operation. For a relational treatment see [9]. All submodules of a
module are pairwise compatible with each other.
2.1 Transformations
In this section we sketch an extension of SDA, intended to cope with some
standard techniques in software refactoring (e.g., [1, 7]). Examples of such tech-
niques are consistent renaming of methods or classes in a large software system.
To stay at the same level of abstraction as before, we realize this by a mechanism
for generally modifying the fragments in SDA modules.
Monoid Modules and Structured Document Algebra 35
By a transformation or modification or refactoring we mean a total function
T : F(V) → F(V). By T · m we denote the application of T to a module m. It yields
a new module defined by
T(m(v)) if v ∈ dom(m)
(T · m)(v) =df
undefined otherwise .
We need to handle the special case of transforming the error fragment . Since
we don’t want to allow transformations to mask errors that are related to mod-
ule addition, we add the requirement
T( ) = .
We use the convention that · binds stronger than all other operators. Note that,
although T is supposed to be a total function on all fragments, it might well
leave many of those unchanged, i.e., act as the identity on them.
2.2 Structure of Transformations
Definition 2.1 A monoid of transformations is a structure F = (F, ◦, 1), where F is
a set of total functions f : X → X over some set X, closed under function com-
position ◦, and 1 the identity function. The pair (X, F) is called transformation
monoid of X. By T|A we denote the transformation T restricted to the set A.
We call the set of transformations on fragments Γ . Then, by the above defini-
tion, (F(V), Γ ) is the transformation monoid of fragments F(V) which we abbre-
viate to Γ . Since these transformations are not necessarily invertible, in general
Γ is not a transformation group. We now can extend the list of properties given
in [2].
(6) T · (m + n) = T · m + n ⇐ T|ran(n) = 1|ran(n) ∧ m ↓ n ,
(7) 1 · m = m ,
(8) T · 0 = 0 .
0 being an annihilator, (Property (8)) means that transformations can only
change existing fragments rather than create new ones.
Furthermore we can define the application equivalence ≈ of two transforma-
tions S, T by S ≈ T ⇔df ∀ m : S · m = T · m.
It is common to undo refactorings, e.g., undo a renaming of a variable. This
can be modelled by inverse transformations, denoted by −1 . When it exists,
the inverse of a stacked, or composed transformation, is given by (T ◦ S)−1 =
S−1 ◦T−1 . Of course the inverse of T or S might not exist, e.g., if T is not injective.
As stated above transformations are total functions. Since they act as the
identity for fragments that should not be modified we define the set of frag-
ments they transform as follows.
Definition 2.2 Let T : F(V) → F(V) be a transformation. Then we call Tm =df
{f ∈ F(V) : T(f) 6= f} the modified fragments of T and Tv =df {T(f) ∈ F(V) :
T(f) 6= f} = ran(T|Tm ) the value set of T.
36 A. Zelend
Restricting transformations to their modified fragments allows us to state
situations in which transformations can be omitted or commute.
Lemma 2.3
1. T · (S · m) = S · m if Tm ⊆ Sm ∧ Tm ∩ Sv = ∅.
2. T and S commute if Tm ∩ Sm = ∅ ∧ Tm ∩ Sv = ∅ ∧ Tv ∩ Sm = ∅.
A proof can be found in Appendix A.1.
3 Abstracting from SDA
The set M of modules, i.e., partial maps m : V F(V), with + and −, defined
as in subsection 2, forms an algebraic structure SDA =df (M, +, −, 0) such that
(M, +, 0) is an idempotent and commutative monoid and which satisfies the fol-
lowing laws for all l, m, n ∈ M:
1. (l − m) − n = l − (m + n) , 3. 0 − l = 0 ,
2. (l + m) − n = (l − n) + (m − l) , 4. l − 0 = l .
Definition 3.1 A monoid module (m-module) is an algebraic structure (B, M, :)
where (M, +, 0) is an idempotent and commutative monoid and (B, +, ·, 0, 1, ¬)
is a Boolean algebra in which 0 and 1 are the least and greatest element and ·
and + denote meet and join. Note that 0 and + are overloaded, like in classi-
cal modules or vector spaces. The restriction, or scalar product, : is a mapping
B × M → M satisfying for all p, q ∈ B and m, n ∈ M:
(p + q) : m = p : m + q : m , (1) (p · q) : m = p : (q : m) , (4)
p : (m + n) = p : m + p : n , (2) 1:m = m , (5)
0:m = 0 , (3) p:0 = 0 . (6)
We define the natural pre-order on (M, +, 0) by m ≤ n ⇔df m + n = n.
Therefore + is isotone in both arguments.
We have choosen the name monoid module following the notion of a mod-
ule over a ring and because SDA’s modules form an idempotent and commu-
tative monoid.
Lemma 3.2
1. Restriction : is isotone in both arguments.
2. p : m ≤ m.
3. p : (q : m) = q : (p : m)
The first claim follows by distributivity, the second by isotony and (5) and
the third by (4) and Boolean algebra.
The structure RMM = (P(M), P(M × N), :), where : is restriction, i.e., p : m =
{(x, y) | x ∈ p ∧ (x, y) ∈ m}, forms a mono module. To model subtraction we
extend mono modules with the predomain operator p : M → B.
Definition 3.3 A predomain monoid module (predomain m-module) is a structure
(B, M, :, p ) such that(B, M, :) is a m-module and p : M → B satisfies for all p ∈ B
and m ∈ M:
Monoid Modules and Structured Document Algebra 37
(d1) m ≤ pm : m , (d2) p(p : m) ≤ p .
In a predomain m-module pm is the least left preserver of m and ¬pa is the great-
est left annihilator. To justify this we present the following lemma.
Lemma 3.4 In a predomain m-module (B, M, :, p ) for all p ∈ B and m ∈ M:
(llp) pm ≤ p ⇔ m ≤ p : m , (gla) p ≤ ¬pm ⇔ p : m ≤ 0 .
Note that (llp) does not establish a Galois connection, since there is no great-
est element in the monoid (M, +, 0) per se, cf. [5] A proof can be found in Ap-
pendix A.2.
Now we can give more useful properties of the predomain function like
isotony or strictness.
Lemma 3.5 In a predomain m-module (B, M, :, p ) for all p ∈ B and m, n ∈ M:
1. m = 0 ⇔ pm = 0 , 4. p(m + n) = pm + pn ,
2. m ≤ n ⇒ pm ≤ pn , 5. p(p : m) : m = p : m ,
3. m = pm : m , 6. p(p : m) = p · pm .
A proof can be found in Appendix A.3.
Now it is easy to verify that the SDA laws for subtractions also hold in a pre-
domain m-module. Note that the sides change, e.g., right distributivity becomes
left distributivity.
Lemma 3.6 Assume a predomain m-module (B, M, :, p ). Then for all l, m, n ∈ M:
1. p(¬pn : m) = pm · ¬pn , 5. ¬p0 : m = m ,
2. (¬pn : 0 = 0) , 6. ¬pm : m = 0 ,
3. ¬pl : (m + n) = ¬pl : m + ¬pl : n , 7. ¬pn : m ≤ m ,
4. ¬p(m + n) : l = ¬pn :(¬pm : l) , 8. m ≤ n ⇒ ¬pn : m = 0 .
A proof can be found in Appendix A.4.
By defining pm =df {x | (x, y) ∈ m} RMM becomes a predomain m-module
and using an RMM over binary functional relations R ⊆ V × F(V), i.e., R˘; R ⊆
id(F(V)), allows us to reason about SDA. As a result, SDA’s subtraction m − n of
modules is equivalent to ¬pn : m in the corresponding RMM.
38 A. Zelend
Using SDA’s module addition, cf. Section 2, we can investigate the induced
natural pre-order.
m ≤ n ⇔df m + n = n
m(v) if v ∈ pm − pn
n(v) if v ∈ pn − pm
⇔ = n(v)
m(v) + n(v) if v ∈ pm ∩ pn
undefined if v 6∈ pm ∪ pn
m(v) = n(v) if v ∈ pm − pn
n(v) = n(v) if v ∈ pn − pm
⇔
m(v) + n(v) = n(v) if v ∈ pm ∩ pn
true if v 6∈ pm ∪ pn
false if v ∈ pm − pn
true if v ∈ pn − pm
⇔
m(v) ≤ n(v) if v ∈ pm ∩ pn
true if v 6∈ pm ∪ pn
⇔ v ∈ pn − pm ∨ (v ∈ pm ∩ pn ∧ m(v) ≤ n(v)) ∨ v 6∈ pm ∪ pn for any v ∈ V.
Therefore the least element w.r.t. ≤ is the empty module 0 and the top element
is the module t with t(v) = for any v ∈ V.
SDA’s overriding operator m −. n can also be defined in a predomain m-
module: m −. n =df m + ¬pm : n . In [6] this operator, embedded into a Kleene
algebra, is used to update links in pointer structures.
Lemma 3.7 In a predomain m-module (B, M, :, p ) for all p ∈ B and l, m, n ∈ M:
1. 0 −. n = n, 4. m = pm :(m −. n),
2. m −. 0 = m, 5. p(m −. n) = pm + pn,
3. m ≤ m −. n, 6. pm ≥ pn ⇒ m −. n = m,
7. l −. (m + n) = l −. m + l −. n.
A proof can be found in Appendix A.5.
Future work will focus on further properties of transformations and their
incorporation into the abstract framework of predomain m-modules.
Acknowledgments I am very grateful to the anonymous referees for helpful
comments and suggestions and I thank B. Möller for fruitful discussions and
valuable comments.
Monoid Modules and Structured Document Algebra 39
References
1. Batory, D.: Program refactorings, program synthesis, and model-driven design. In:
Krishnamurthi, S., Odersky, M. (eds.) Compiler Construction. LNCS, vol. 4420, pp.
156–171. Springer (2007)
2. Batory, D., Höfner, P., Möller, B., Zelend, A.: Features, modularity, and variation
points. Tech. Rep. CS-TR-13-14, The University of Texas at Austin (2013)
3. Batory, D., O’Malley, S.: The design and implementation of hierarchical software
systems with reusable components. ACM Transactions Software Engineering and
Methodology 1(4), 355–398 (1992)
4. Dang, H.H., Glück, R., Möller, B., Roocks, P., Zelend, A.: Exploring modal
worlds. Journal of Logical and Algebraic Methods in Programming 83(2), 135 –
153 (2014), http://www.sciencedirect.com/science/article/pii/S1567832614000058,
festschrift in Honour of Gunther Schmidt on the Occasion of his 75th Birthday
5. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Com-
put. Log. 7(4), 798–833 (2006), http://doi.acm.org/10.1145/1183278.1183285
6. Ehm, T.: The Kleene Algebra of Nested Pointer Structures: Theory and Applications.
Ph.D. thesis, Universität Augsburg (2005)
7. Kuhlemann, M., Batory, D., Apel, S.: Refactoring feature modules. In: Edwards, S.,
Kulczycki, G. (eds.) Formal Foundations of Reuse and Domain Engineering. LNCS,
vol. 5791, pp. 106–115. Springer (2009)
8. Lopez-Herrejon, R., Batory, D.: A standard problem for evaluating product-line
methodologies. In: Bosch, J. (ed.) GCSE ’01: Generative and Component-Based Soft-
ware Engineering. LNCS, vol. 2186, pp. 10–24. Springer (2001)
9. Möller, B.: Towards pointer algebra. Sci. Comput. Program. 21(1), 57–90 (1993),
http://dx.doi.org/10.1016/0167-6423(93)90008-D
A Proofs for Subsection 2.2 and Section 3
A.1 Proofs for Lemma 2.3
1. Tm ∩ Sv = ∅ implies that T acts as the identity on the set Sv . Since Tm ⊆ Sm ,
we obtain that T also is the identity on the set ran(m) − Sm . Therefore we
have T · (S · m)(v) = T · (S(m(v))) = S(m(v)).
2. We have x ∈ Sm ⇒ T(x) = x ∧ x ∈ Tm ⇒ S(x) = x because Tm ∩ Sm = ∅.
Therefore, for an arbitrary x = m(v), we get
S(x) if x ∈ Sm since Tm ∩ Sv = ∅ ,
(T ◦ S)(x) = T(S(x)) = T(x) if x ∈ Tm ,
x if x ∈ Sm ∩ Tm .
On the other hand we get
T(x) if x ∈ Tm since Sm ∩ Tv = ∅ ,
(S ◦ T)(x) = S(T(x)) = S(x) if x ∈ Sm ,
x if x ∈ Tm ∩ Sm .
40 A. Zelend
A.2 Proofs for Lemma 3.4
(llp) ⇒: m ≤ pm : m ≤ p : m by (d1) and isotony of restriction (pm ≤ p).
⇐: m ≤ p : m ⇒ m = p : m by Lemma 3.2.2 and therefore pm = p(p : m) ≤ p
by (d2).
(gla) ⇒: p : m ≤ p :(pm : m) = (p · pm) : m by (d1), isotony of restriction and (4).
Since p ≤ ¬pm, p · pm = 0 holds and therefore (p · pm) : m = 0 : m = 0 by (3).
⇐: m = 1 : m = (p + ¬p) : m = p : m + ¬p : m = 0 + ¬p : m = ¬p : m by (5),
Boolean algebra, (1) and the assumption (p : m ≤ 0). Using (llp) we have
pm ≤ ¬p which is equivalent to p ≤ ¬pm by shunting.
A.3 Proofs for Lemma 3.5
1. ⇒: pm = p0 = p(0 : 0) ≤ 0 by (3) and (d2).
⇐: m ≤ pm : m by (d1) and therefore m ≤ 0 : m = 0 by (3).
2. ¬pn ≤ ¬pn ⇒ ¬pn : n ≤ 0 ⇒ ¬pn : m ≤ 0 ⇒ ¬pn ≤ ¬pm ⇒ pm ≤ pn by (gla),
isotony of restriction, (gla) again and shunting (2 times).
3. p ≤ ¬p(m + n) ⇔ p : (m + n) ≤ 0 ⇔ p : m + p : n ≤ 0 ⇔ p : m ≤ 0 ∧ p : n ≤
0 ⇔ p ≤ ¬pm ∧ p ≤ ¬pn ⇔ p ≤ ¬pm · ¬pn ⇔ p ≤ ¬(pm + pn). Using indirect
equality we get ¬p(m + n) = ¬(pm + pm) ⇔ p(m + n) = pm + pm.
4. m ≤ pm : m holds by (d1) and pm : m ≤ m holds by Lemma 3.2.2.
5. ≤: p(p : m) : m ≤ p : m holds by (d2) and isotony of restriction.
≥: p : m ≤ p(p : m) :(p : m) = (p(p : m) · p) : m by (d1) and (4). Since p(p : m) ≤ p
by (d2) it follows that p(p : m) · p = p(p : m). In sum we have p : m ≤ p(p : m) : m.
6. First we have pm = p(1 : m) = p((p + ¬p) : m) = p(p : m + ¬p : m) = p(p : m) +
p(¬p : m) by (5), Boolean algebra, and Part 4. By (d2) it holds that p(p : m) ≤
p ∧ p(¬p : m) ≤ ¬p. And therefore by Boolean algebra: p · p(p : m) = p(p : m)
and p · p(¬p : m) = 0. In sum we conclude: p · pm = p · (p(p : m) + p(¬p : m)) =
p · p(p : m) + p · p(¬p : m) = p · p(p : m) + 0 = p(p : m).
A.4 Proofs for Lemma 3.6
1. p(¬pn : m) = pm · ¬pn by Lemma 3.5.6 and Boolean algebra.
2. (¬pn : 0 = 0) by (6).
3. ¬pl : (m + n) = ¬pl : m + ¬pl : n by (5).
4. ¬p(m + n) : l = ¬(pm + pn) : l = (¬pm · ¬pn) = ¬pm :(¬pn : l) = ¬pm :(¬pn : l) by
Lemma 3.5.4, Boolean algebra, (4) and Lemma 3.2.3.
5. ¬p0 : m = ¬0 : m = 1 : m = m by (5) and ¬p0 = ¬0 = 1 Lemma 3.5.1, Boolean
algebra and (5).
6. ¬pm ≤ ¬pm ⇒ ¬pm : m ≤ 0 by (gla).
7. ¬pn : m ≤ m by Lemma 3.2.2.
8. m ≤ n ⇒ pm ≤ pn ⇒ ¬pn ≤ ¬pm ⇒ ¬pn : m ≤ 0 by Lemma 3.5.2, Boolean
algebra and (gla).
Monoid Modules and Structured Document Algebra 41
A.5 Proofs for Lemma 3.7
1. 0 −. n = 0 + ¬p0 : n = ¬0 : n = 1 : n = n by Lemma 3.5.1 and (5).
2. m −. 0 = m + ¬pm : 0 = m + 0 = m by (6).
3. m ≤ m + ¬pm : n = m −. n by isotony of +.
4. pm :(m −. n) = pm :(m + ¬pm : n) = pm : m + pm :(¬pm : n) = m + (pm · ¬pm) : n =
m + 0 : n = m + 0 = m by (2), (4) and (3).
5. p(m −. n) = p(m + ¬pm : n) = pm + p(¬pm : n) = pm + ¬pm · pn = pm + pn ,
by Lemma 3.5.4, 3.5.6 and Boolean algebra.
6. First we conclude pm ≥ pn ⇒ ¬pm ≤ ¬pn ⇒ ¬pm : n ≤ 0 by (gla). Therefore
m −. n = m + ¬pm : n = m + 0 = m.
7. l −. (m+n) = l+¬pl :(m+n) = l+¬pl : m+¬pl : n = l+¬pl : m+l+¬pl : n =
l −. m + l −. n by (2) and idempotence.