/[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 93378 - (show annotations)
Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File size: 7060 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 children_set[c]
71 not up[c]
72 across up as p all p.item.is_wrapped end
73
74 modify ([Current, c])
75 modify_field ("value", up)
76 modify (children_set)
77 do
78 unwrap -- default: public
79 c.unwrap
80 unwrap_all (children_set)
81 if parent /= Void then
82 parent.unwrap
83 end
84
85 check across children_set as o all not o.item.children_set.has (c) end end
86 check across children_set as o all across children_set as v all o.item /= v.item implies o.item.children_set.is_disjoint (v.item.children_set) end end end
87
88 children.extend_back (c) -- preserves parent
89 set_subjects (subjects & c)
90 set_observers (observers & c)
91 c.set_parent (Current)
92 c.set_subjects (c.subjects & Current)
93 c.set_observers (c.observers & Current)
94
95 check across children_set as o all o.item.inv_only ("value_consistent") end end
96 check c.inv_only ("value_consistent") end
97 children_set := children_set & c
98 check across children_set as o all o.item.inv_only ("value_consistent") end end
99
100 wrap_all (children_set)
101 update (c)
102
103 if parent /= Void then
104 parent.wrap
105 end
106
107 wrap -- default: public
108 ensure
109 children.has (c)
110 c.value = old c.value
111
112 is_wrapped -- default: public
113 across observers as o all o.item.is_wrapped end -- default: public
114 c.is_wrapped -- default: public
115 across c.observers as o all o.item.is_wrapped end -- default: public
116
117 false
118 end
119
120 feature {F_COM_COMPOSITE_D}
121
122 set_parent (p: F_COM_COMPOSITE_D)
123 require
124 is_open -- default: not public
125 across observers as o all o.item.is_open end -- default: not public
126
127 parent = Void
128 children_set.is_empty
129 p /= Void
130
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 owns = [children]
152 children.is_wrapped
153 across children_set as o all o.item.is_wrapped end
154
155 inv_without ("value_consistent") -- All invariant clauses except "value_consistent"
156 across up as p all p.item.is_wrapped end
157 is_max (value, children_set / c)
158
159 modify_field ("value", [Current, up])
160 modify_field ("closed", children_set)
161 modify (children)
162 decreases (up)
163 do
164 if value < c.value then
165 if parent /= Void then
166 check up [parent] end
167 check parent.is_wrapped end
168 parent.unwrap
169 end
170 unwrap_all (children_set)
171 lemma1 (children_set, value, c)
172 check is_max (value, children_set / c) end
173 value := c.value -- preserves children
174 check is_max (value, children_set) end
175
176 -- check across children_set as x all x.item.inv_only ("value_consistent") end end
177 -- check across children_set as x all x.item.inv_without ("value_consistent") end end
178 -- check across children_set as x all x.item.inv_only ("i1", "i2", "i3", "i4") end end
179 -- check across children_set as x all x.item.inv_only ("i5", "i6", "i7", "i8") end end
180 -- check across children_set as x all x.item.inv_only ("i9", "i10") end end
181 -- check across children_set as x all x.item.inv_only ("i11", "i12") end end
182 -- check across children_set as x all x.item.inv_only ("i13") end end
183 wrap_all (children_set)
184 if parent /= Void then
185 parent.update (Current)
186 end
187 end
188
189 check
190 i1: children /= Void
191 i2: children_set = children.sequence
192 i3: not children_set[Current]
193 i3: not children_set[children]
194 i4: parent /= Current
195 i5: parent /= Void implies not (children_set[parent])
196 i6: across children_set as x all x.item /= Void and then x.item.parent = Current end
197 i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity
198 i8: parent = Void implies up.is_empty
199 value_consistent: is_max (value, children_set)
200 i9: parent = Void implies subjects = children_set
201 i9: parent /= Void implies subjects = children_set & parent
202 i10: parent = Void implies observers = children_set
203 i10: parent /= Void implies observers = children_set & parent
204 i11: owns = [children]
205 i12: across subjects as s all s.item.observers.has (Current) end -- default
206 i13: not children_set[Void]
207 end
208 wrap
209 ensure
210 is_wrapped
211 end
212
213
214 lemma1 (set: MML_SET [F_COM_COMPOSITE_D]; v: INTEGER; c: F_COM_COMPOSITE_D)
215 note
216 -- status: ghost
217 require
218 set[c]
219 is_max (v, set / c)
220 c.value > v
221
222 modify ([])
223 do
224 ensure
225 is_max (c.value, set)
226 end
227
228 invariant
229 i1: children /= Void
230 i2: children_set = children.sequence
231 i3: not children_set[Current]
232 i3: not children_set[children]
233 i4: parent /= Current
234 i5: parent /= Void implies not (children_set[parent])
235 i6: across children_set as ic all ic.item /= Void and then ic.item.parent = Current end
236 i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity
237 i8: parent = Void implies up.is_empty
238 value_consistent: is_max (value, children_set)
239 i9: parent = Void implies subjects = children_set
240 i9: parent /= Void implies subjects = children_set & parent
241 i10: parent = Void implies observers = children_set
242 i10: parent /= Void implies observers = children_set & parent
243 i11: owns = [children]
244 i12: across subjects as s all s.item.observers.has (Current) end -- default
245 i13: not children_set[Void]
246 i14: across children_set as ic all attached {F_COM_COMPOSITE_D} ic.item end
247
248 note
249 explicit: subjects, observers
250
251 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23