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

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

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 93377 by julian, Wed Nov 13 17:15:59 2013 UTC revision 93378 by julian, Thu Nov 14 15:57:08 2013 UTC
# Line 16  feature Line 16  feature
16          value: INTEGER          value: INTEGER
17    
18          up, children_set: MML_SET [F_COM_COMPOSITE_D]          up, children_set: MML_SET [F_COM_COMPOSITE_D]
19                          -- Set of transitive parents and children                          -- Set of transitive parents and non-transitive children
20                  note                  note
21                          status: ghost                          status: ghost
22                  attribute                  attribute
# Line 82  feature Line 82  feature
82                                  parent.unwrap                                  parent.unwrap
83                          end                          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                          children.extend_back  (c) -- preserves parent
89                          set_subjects (subjects & c)                          set_subjects (subjects & c)
90                          set_observers (observers & c)                          set_observers (observers & c)
# Line 92  feature Line 95  feature
95                          check across children_set as o all o.item.inv_only ("value_consistent") end end                          check across children_set as o all o.item.inv_only ("value_consistent") end end
96                          check c.inv_only ("value_consistent") end                          check c.inv_only ("value_consistent") end
97                          children_set := children_set & c                          children_set := children_set & c
98                          check assume: across children_set as o all o.item.inv_only ("value_consistent") end end                          check across children_set as o all o.item.inv_only ("value_consistent") end end
99    
100                          wrap_all (children_set)                          wrap_all (children_set)
101                          update (c)                          update (c)
# Line 122  feature {F_COM_COMPOSITE_D} Line 125  feature {F_COM_COMPOSITE_D}
125                          across observers as o all o.item.is_open end -- default: not public                          across observers as o all o.item.is_open end -- default: not public
126    
127                          parent = Void                          parent = Void
128                          children.is_empty                          children_set.is_empty
129                          p /= Void                          p /= Void
130    
131                          modify_field (["parent", "up"], Current)                          modify_field (["parent", "up"], Current)
# Line 165  feature {F_COM_COMPOSITE_D} Line 168  feature {F_COM_COMPOSITE_D}
168                                          parent.unwrap                                          parent.unwrap
169                                  end                                  end
170                                  unwrap_all (children_set)                                  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                                  value := c.value  -- preserves children
174                                  check is_max (value, children_set) end                                  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)                                  wrap_all (children_set)
184                                  if parent /= Void then                                  if parent /= Void then
185                                          parent.update (Current)                                          parent.update (Current)
186                                  end                                  end
187                          end                          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                          wrap
209                  ensure                  ensure
210                          is_wrapped                          is_wrapped
211                  end                  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  invariant
229          i1: children /= Void          i1: children /= Void
230          i2: children_set = children.sequence          i2: children_set = children.sequence
231          i3: not children_set[Current]          i3: not children_set[Current]
232          i4: not children_set[children]          i3: not children_set[children]
233            i4: parent /= Current
234          i5: parent /= Void implies not (children_set[parent])          i5: parent /= Void implies not (children_set[parent])
235          i6: across children_set as c all c.item /= Void and then c.item.parent = Current end          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          i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity
237          i8: parent = Void implies up.is_empty          i8: parent = Void implies up.is_empty
238          value_consistent: is_max (value, children_set)          value_consistent: is_max (value, children_set)
239          i9: subjects = children_set & parent  / Void          i9: parent = Void implies subjects = children_set
240          i10: observers = children_set & parent / Void          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]          i11: owns = [children]
244          i12: across subjects as s all s.item.observers.has (Current) end -- default          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  note
249          explicit: subjects, observers          explicit: subjects, observers

Legend:
Removed from v.93377  
changed lines
  Added in v.93378

  ViewVC Help
Powered by ViewVC 1.1.23