/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_composite_d.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_composite_d.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93405 - (show annotations)
Fri Nov 15 21:07:40 2013 UTC (5 years, 11 months ago) by julian
File size: 5863 byte(s)
AutoProof: continued ownership implementation.

1 note
2 description: "Composite with no-orphans and acyclicity invariants, and optimized update."
3 explicit: "all"
4
5 class F_COM_COMPOSITE_D
6
7 create
8 make
9
10 feature
11
12 children: F_COM_LIST [F_COM_COMPOSITE_D]
13
14 parent: F_COM_COMPOSITE_D
15
16 value: INTEGER
17
18 up, children_set: MML_SET [F_COM_COMPOSITE_D]
19 -- Set of transitive parents and non-transitive children
20 note
21 status: ghost
22 attribute
23 end
24
25 is_max (v: INTEGER; nodes: MML_SET [F_COM_COMPOSITE_D]): BOOLEAN
26 note
27 status: ghost
28 require
29 reads (nodes)
30 modify ([])
31 do
32 Result :=
33 across nodes as n all n.item.value <= v end and
34 (nodes.is_empty or across nodes as n some n.item.value = v end)
35 end
36
37 make (v: INTEGER)
38 note
39 status: creator
40 require
41 is_open -- default: creator
42
43 modify (Current) -- default: creator
44 do
45 up := {MML_SET [F_COM_COMPOSITE_D]}.empty_set
46 children_set := {MML_SET [F_COM_COMPOSITE_D]}.empty_set
47 create children.make
48 set_owns ([children])
49 value := v
50 wrap -- default: creator
51 ensure
52 is_wrapped -- default: creator
53 across observers as o all o.item.is_wrapped end -- default: creator
54 value = v
55 parent = Void
56 children.is_empty
57 end
58
59 add_child (c: F_COM_COMPOSITE_D)
60 require
61 is_wrapped -- default: public
62 across observers as o all o.item.is_wrapped end -- default: public
63 c.is_wrapped -- default: public
64 across c.observers as o all o.item.is_wrapped end -- default: public
65
66 c /= Void
67 c /= Current
68 c.parent = Void
69 c.children.is_empty
70 not up[c]
71 across up as p all p.item.is_wrapped end
72
73 modify ([Current, c])
74 modify_field (["value", "closed"], up)
75 modify (children_set)
76 do
77 unwrap -- default: public
78 c.unwrap
79 if parent /= Void then
80 parent.unwrap
81 end
82
83 check across children_set as o all o.item.is_wrapped end end
84 children.extend_back (c) -- preserves parent
85 set_subjects (subjects & c)
86 set_observers (observers & c)
87 c.set_parent (Current)
88 c.set_subjects (c.subjects & Current)
89 c.set_observers (c.observers & Current)
90 check across children_set as o all o.item.is_wrapped end end
91 check false end
92 unwrap_all (children_set)
93 children_set := children_set & c
94
95 check across children_set as o all o.item.inv_only ("i1", "i2") end end
96 check false end
97
98 wrap_all (children_set)
99 if parent /= Void then
100 parent.wrap
101 end
102
103 update (c)
104
105 wrap -- default: public
106 ensure
107 children.has (c)
108 c.value = old c.value
109 children_set = old children_set & c
110 up = old up
111 across up as p all p.item.is_wrapped end
112
113 is_wrapped -- default: public
114 across observers as o all o.item.is_wrapped end -- default: public
115 c.is_wrapped -- default: public
116 across c.observers as o all o.item.is_wrapped end -- default: public
117 end
118
119 feature {F_COM_COMPOSITE_D}
120
121 set_parent (p: F_COM_COMPOSITE_D)
122 require
123 is_open -- default: not public
124 across observers as o all o.item.is_open end -- default: not public
125
126 parent = Void
127 children_set.is_empty
128 p /= Void
129
130 modify (Current)
131 modify_field (["parent", "up"], Current)
132 do
133 parent := p
134 up := p.up & p
135 ensure
136 parent = p
137 up = p.up & p
138
139 is_open -- default: not public
140 across observers as o all o.item.is_open end -- default: not public
141 end
142
143 update (c: F_COM_COMPOSITE_D)
144 -- Update values of Current and transitive parents taking into account new child `c'.
145 note
146 explicit: contracts
147 require
148 c /= Void
149 children_set[c]
150 is_open
151 children.is_wrapped
152 across up as p all p.item.is_wrapped end
153
154 inv_without ("value_consistent")
155
156 -- not (children_set / c).is_empty implies is_max (value, children_set / c)
157 -- is_max (value, children_set / c) or is_max (c.value, children_set)
158
159 modify_field (["value", "closed"], [Current, up])
160 decreases (up)
161 do
162 if
163 ((children_set / c).is_empty and value /= c.value) or
164 value < c.value
165 then
166 if parent /= Void then
167 parent.unwrap
168 end
169 value := c.value
170 wrap
171 if parent /= Void then
172 parent.update (Current)
173 end
174 else
175 check value >= c.value end
176 check is_max (value, children_set) end
177 wrap
178 end
179 -- check assume: false end
180
181
182 -- if value < c.value then
183 -- check assume: false end
184 -- if parent /= Void then
185 -- parent.unwrap
186 -- end
187 -- value := c.value -- preserves children
188 -- wrap
189 -- if parent /= Void then
190 -- parent.update (Current)
191 -- end
192 -- elseif (children_set / c).is_empty then
193 -- if parent /= Void then
194 -- parent.unwrap
195 -- end
196 -- value := c.value
197 -- check is_max (value, children_set) end
198 -- wrap
199 -- if parent /= Void then
200 -- parent.update (Current)
201 -- end
202 -- else
203 -- check assume: false end
204 -- end
205 ensure
206 is_wrapped
207 across up as p all p.item.is_wrapped end
208 -- across children_set as o all o.item.is_wrapped end
209 -- has_to_fail: false
210 end
211
212 invariant
213 value_consistent: is_max (value, children_set)
214
215 i1: children /= Void
216 i2: children_set = children.sequence
217 i3: not children_set[Current]
218 i3: not children_set[children] and not up[children]
219 i4: parent /= Current
220 i5: parent /= Void implies not (children_set[parent])
221 i6: across children_set as ic all ic.item /= Void and then ic.item.parent = Current end
222 i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity
223 i8: parent = Void implies up.is_empty
224 i9: parent = Void implies subjects = children_set
225 i9: parent /= Void implies subjects = children_set & parent
226 i10: parent = Void implies observers = children_set
227 i10: parent /= Void implies observers = children_set & parent
228 i11: owns = [children]
229 i12: across subjects as s all s.item.observers.has (Current) end -- default
230 i13: not children_set[Void]
231 i14: across children_set as ic all ic.item.generating_type = {F_COM_COMPOSITE_D} end
232
233 note
234 explicit: subjects, observers
235
236 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23