/[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 93404 by julian, Thu Nov 14 15:57:08 2013 UTC revision 93405 by julian, Fri Nov 15 21:07:40 2013 UTC
# Line 67  feature Line 67  feature
67                          c /= Current                          c /= Current
68                          c.parent = Void                          c.parent = Void
69                          c.children.is_empty                          c.children.is_empty
                         not children_set[c]  
70                          not up[c]                          not up[c]
71                          across up as p all p.item.is_wrapped end                          across up as p all p.item.is_wrapped end
72    
73                          modify ([Current, c])                          modify ([Current, c])
74                          modify_field ("value", up)                          modify_field (["value", "closed"], up)
75                          modify (children_set)                          modify (children_set)
76                  do                  do
77                          unwrap -- default: public                          unwrap -- default: public
78                          c.unwrap                          c.unwrap
                         unwrap_all (children_set)  
79                          if parent /= Void then                          if parent /= Void then
80                                  parent.unwrap                                  parent.unwrap
81                          end                          end
82    
83                          check across children_set as o all not o.item.children_set.has (c) end end                          check across children_set as o all o.item.is_wrapped end end
                         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  
   
84                          children.extend_back  (c) -- preserves parent                          children.extend_back  (c) -- preserves parent
85                          set_subjects (subjects & c)                          set_subjects (subjects & c)
86                          set_observers (observers & c)                          set_observers (observers & c)
87                          c.set_parent (Current)                          c.set_parent (Current)
88                          c.set_subjects (c.subjects & Current)                          c.set_subjects (c.subjects & Current)
89                          c.set_observers (c.observers & Current)                          c.set_observers (c.observers & Current)
90                            check across children_set as o all o.item.is_wrapped end end
91                          check across children_set as o all o.item.inv_only ("value_consistent") end end                          check false end
92                          check c.inv_only ("value_consistent") end                          unwrap_all (children_set)
93                          children_set := children_set & c                          children_set := children_set & c
                         check across children_set as o all o.item.inv_only ("value_consistent") end end  
94    
95                          wrap_all (children_set)                          check across children_set as o all o.item.inv_only ("i1", "i2") end end
96                          update (c)                          check false end
97    
98                            wrap_all (children_set)
99                          if parent /= Void then                          if parent /= Void then
100                                  parent.wrap                                  parent.wrap
101                          end                          end
102    
103                            update (c)
104    
105                          wrap -- default: public                          wrap -- default: public
106                  ensure                  ensure
107                          children.has (c)                          children.has (c)
108                          c.value = old c.value                          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                          is_wrapped -- default: public
114                          across observers as o all o.item.is_wrapped end -- default: public                          across observers as o all o.item.is_wrapped end -- default: public
115                          c.is_wrapped -- default: public                          c.is_wrapped -- default: public
116                          across c.observers as o all o.item.is_wrapped end -- default: public                          across c.observers as o all o.item.is_wrapped end -- default: public
   
                         false  
117                  end                  end
118    
119  feature {F_COM_COMPOSITE_D}  feature {F_COM_COMPOSITE_D}
# Line 128  feature {F_COM_COMPOSITE_D} Line 127  feature {F_COM_COMPOSITE_D}
127                          children_set.is_empty                          children_set.is_empty
128                          p /= Void                          p /= Void
129    
130                            modify (Current)
131                          modify_field (["parent", "up"], Current)                          modify_field (["parent", "up"], Current)
132                  do                  do
133                          parent := p                          parent := p
# Line 148  feature {F_COM_COMPOSITE_D} Line 148  feature {F_COM_COMPOSITE_D}
148                          c /= Void                          c /= Void
149                          children_set[c]                          children_set[c]
150                          is_open                          is_open
                         owns = [children]  
151                          children.is_wrapped                          children.is_wrapped
                         across children_set as o all o.item.is_wrapped end  
   
                         inv_without ("value_consistent") -- All invariant clauses except "value_consistent"  
152                          across up as p all p.item.is_wrapped end                          across up as p all p.item.is_wrapped end
                         is_max (value, children_set / c)  
153    
154                          modify_field ("value", [Current, up])                          inv_without ("value_consistent")
155                          modify_field ("closed", children_set)  
156                          modify (children)  --                      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)                          decreases (up)
161                  do                  do
162                          if value < c.value then                          if
163                                    ((children_set / c).is_empty and value /= c.value) or
164                                    value < c.value
165                            then
166                                  if parent /= Void then                                  if parent /= Void then
                                         check up [parent] end  
                                         check parent.is_wrapped end  
167                                          parent.unwrap                                          parent.unwrap
168                                  end                                  end
169                                  unwrap_all (children_set)                                  value := c.value
170                                  lemma1 (children_set, value, c)                                  wrap
                                 check is_max (value, children_set / c) end  
                                 value := c.value  -- preserves children  
                                 check is_max (value, children_set) end  
   
 --                              check across children_set as x all x.item.inv_only ("value_consistent") end end  
 --                              check across children_set as x all x.item.inv_without ("value_consistent") end end  
 --                              check across children_set as x all x.item.inv_only ("i1", "i2", "i3", "i4") end end  
 --                              check across children_set as x all x.item.inv_only ("i5", "i6", "i7", "i8") end end  
 --                              check across children_set as x all x.item.inv_only ("i9", "i10") end end  
 --                              check across children_set as x all x.item.inv_only ("i11", "i12") end end  
 --                              check across children_set as x all x.item.inv_only ("i13") end end  
                                 wrap_all (children_set)  
171                                  if parent /= Void then                                  if parent /= Void then
172                                          parent.update (Current)                                          parent.update (Current)
173                                  end                                  end
174                            else
175                                    check value >= c.value end
176                                    check is_max (value, children_set) end
177                                    wrap
178                          end                          end
179    --                      check assume: false end
180    
 check  
         i1: children /= Void  
         i2: children_set = children.sequence  
         i3: not children_set[Current]  
         i3: not children_set[children]  
         i4: parent /= Current  
         i5: parent /= Void implies not (children_set[parent])  
         i6: across children_set as x all x.item /= Void and then x.item.parent = Current end  
         i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity  
         i8: parent = Void implies up.is_empty  
         value_consistent: is_max (value, children_set)  
         i9: parent = Void implies subjects = children_set  
         i9: parent /= Void implies subjects = children_set & parent  
         i10: parent = Void implies observers = children_set  
         i10: parent /= Void implies observers = children_set & parent  
         i11: owns = [children]  
         i12: across subjects as s all s.item.observers.has (Current) end -- default  
         i13: not children_set[Void]  
 end  
                         wrap  
                 ensure  
                         is_wrapped  
                 end  
   
   
         lemma1 (set: MML_SET [F_COM_COMPOSITE_D]; v: INTEGER; c: F_COM_COMPOSITE_D)  
                 note  
 --                      status: ghost  
                 require  
                         set[c]  
                         is_max (v, set / c)  
                         c.value > v  
181    
182                          modify ([])  --                      if value < c.value then
183                  do  --                              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                  ensure
206                          is_max (c.value, set)                          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                  end
211    
212  invariant  invariant
213            value_consistent: is_max (value, children_set)
214    
215          i1: children /= Void          i1: children /= Void
216          i2: children_set = children.sequence          i2: children_set = children.sequence
217          i3: not children_set[Current]          i3: not children_set[Current]
218          i3: not children_set[children]          i3: not children_set[children] and not up[children]
219          i4: parent /= Current          i4: parent /= Current
220          i5: parent /= Void implies not (children_set[parent])          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          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          i7: parent /= Void implies (not up[Current] and up = parent.up & parent) -- implies acyclicity
223          i8: parent = Void implies up.is_empty          i8: parent = Void implies up.is_empty
         value_consistent: is_max (value, children_set)  
224          i9: parent = Void implies subjects = children_set          i9: parent = Void implies subjects = children_set
225          i9: parent /= Void implies subjects = children_set & parent          i9: parent /= Void implies subjects = children_set & parent
226          i10: parent = Void implies observers = children_set          i10: parent = Void implies observers = children_set
# Line 243  invariant Line 228  invariant
228          i11: owns = [children]          i11: owns = [children]
229          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
230          i13: not children_set[Void]          i13: not children_set[Void]
231          i14: across children_set as ic all attached {F_COM_COMPOSITE_D} ic.item end          i14: across children_set as ic all ic.item.generating_type = {F_COM_COMPOSITE_D} end
232    
233  note  note
234          explicit: subjects, observers          explicit: subjects, observers

Legend:
Removed from v.93404  
changed lines
  Added in v.93405

  ViewVC Help
Powered by ViewVC 1.1.23