Repository navigation
Expand file tree
/
Copy pathmoveValueDef.als
More file actions
151 lines (119 loc) · 5.77 KB
/
Copy pathmoveValueDef.als
File metadata and controls
151 lines (119 loc) · 5.77 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
open model
pred moveProperty[vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State]{
//k1 -> k3
//k2 -> k4
k3 not in s1.classes
k4 not in s1.classes
k1 in s1.classes
k2 in s1.classes
s2.classes = (s1.classes - k1 - k2) + k3 + k4
k1.name = k3.name
k2.name = k4.name
k1.parentName= k3.parentName
k2.parentName= k4.parentName
vd in k1.structure.elems and vd not in k2.structure.elems
vd not in k3.structure.elems and vd in k4.structure.elems
k4.structure = k2.structure.add[vd]
//k1 -> k3 structure
let idx = k1.structure.idxOf[vd] {
idx = 0 implies k3.structure = rest[k1.structure] else
idx = k1.structure.lastIdx implies k3.structure = k1.structure.subseq[0, idx-1] else
k3.structure = k1.structure.subseq[0, idx-1].append[ k1.structure.subseq[idx+1, k1.structure.lastIdx]]
}
#k1.instances = #k3.instances
#k2.instances = #k4.instances
//k1->k3 instances
all r3 : Instance |
r3 in k3.instances implies one r1 : Instance {
r1 in k1.instances and r1.id = r3.id and
let idx = k1.structure.idxOf[vd], last = k1.structure.lastIdx {
idx = 0 implies r3.items = rest[r1.items] else
idx = last implies r3.items = r1.items.subseq[0, idx-1] else
r3.items = r1.items.subseq[0, idx-1].append[r1.items.subseq[idx+1, last]]
}
}
#k1.instances = #k2.instances or (#k1.instances = 0 and #k2.instances > 0)
#k1.instances = #k2.instances implies {
all r4 : Instance |
r4 in k4.instances implies one r1, r2 : Instance {
r1 in k1.instances and r2 in k2. instances and r1.id = r2.id and r1.id = r4.id and
let idx = k1.structure.idxOf[vd] | r4.items = r2.items.append[r1.items.subseq[idx, idx]]
}
}
#k1.instances = 0 and #k2.instances > 0 implies {
all r4 : Instance |
r4 in k4.instances implies one r2 : Instance {
r2 in k2. instances and r2.id = r4.id and r4.items.subseq[0, add[#r2.items,-1]] = r2.items
and add[#r2.items, 1] = #r4.items
}
}
//reference update not neccesary
}
//run moveProperty for 3 but exactly 2 State, 4 Class, 0 Instance
pred moveProperty_no_record[vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State]{
#k1.instances = 0 and #k2.instances = 0 and (k1.structure.elems & k2.structure.elems) = none and moveProperty[vd, k1, k2, k3, k4, s1, s2]
}
run moveProperty_no_record for 3 but exactly 2 State, 4 Class
pred moveProperty_one_record_in_both[vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State]{
#k1.instances = 1 and #k2.instances = 1 and (k1.structure.elems & k2.structure.elems) = none and moveProperty[vd, k1, k2, k3, k4, s1, s2]
}
run moveProperty_one_record_in_both for 4 but exactly 2 State, 4 Class
pred moveProperty_one_record_in_target_only[vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State]{
#k1.instances = 0 and #k2.instances = 1 and (k1.structure.elems & k2.structure.elems) = none and moveProperty[vd, k1, k2, k3, k4, s1, s2]
}
run moveProperty_one_record_in_target_only for 4 but exactly 2 State, 4 Class
/* ***************************************************************************************** */
assert moveProperty_structure_same{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#s1.classes.structure.elems = #s2.classes.structure.elems
}
check moveProperty_structure_same for 5
assert moveProperty_number_of_valueDefs_same{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#({vc : Property | vc in s1.classes.structure.elems}) = #({vc : Property | vc in s2.classes.structure.elems})
}
check moveProperty_number_of_valueDefs_same for 5
assert moveProperty_number_of_referenceDefs_same_after{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#({rd : Reference | rd in s1.classes.structure.elems}) = #({vc : Reference | vc in s2.classes.structure.elems})
}
check moveProperty_number_of_referenceDefs_same_after for 5
assert moveProperty_number_of_classes_is_same{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#({k : Class | k in s1.classes}) = #({k : Class | k in s2.classes})
}
check moveProperty_number_of_classes_is_same for 5
assert moveProperty_can_increase_number_of_values{ //because they are NOTNULL
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#({k : ValueContainer | k in s1.classes.instances.items.elems}) <= #({k : ValueContainer | k in s2.classes.instances.items.elems})
}
check moveProperty_can_increase_number_of_values for 5
assert moveProperty_not_change_number_of_references{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
#({k : ReferenceContainer | k in s1.classes.instances.items.elems}) = #({k : ReferenceContainer | k in s2.classes.instances.items.elems})
}
check moveProperty_not_change_number_of_references for 5
assert moveProperty_not_change_inheritace_depth{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
depth_preserved[s1, s2]
}
check moveProperty_not_change_inheritace_depth for 5
assert moveProperty_not_change_number_of_children{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
children_preserve[s1,s2]
}
check moveProperty_not_change_number_of_children for 5
assert moveProperty_not_change_cohesion_number{
all vd : Property, disj k1, k2, k3, k4 : Class, disj s1, s2 : State |
moveProperty[vd, k1, k2, k3, k4, s1, s2] implies
coupling_preserve[s1, s2]
}
check moveProperty_not_change_cohesion_number for 5