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

Diff of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_client.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 12  feature Line 12  feature
12                          across c1.up as o all o.item.is_wrapped end                          across c1.up as o all o.item.is_wrapped end
13                          across c1.observers as o all o.item.is_wrapped end                          across c1.observers as o all o.item.is_wrapped end
14    
15                          modify ([c1, c2])                          modify ([c1, c2, c1.up, c1.children_set])
16                  local                  local
17                          c_new: F_COM_COMPOSITE_D                          c_new: F_COM_COMPOSITE_D
18                  do                  do
19                          create c_new.make (10)                          create c_new.make (10)
   
                         check c_new.parent = Void end  
                         check c_new.children_set.is_empty end  
   
                         check not c1.up.has (c_new) end  
                         check not c1.children_set.has (c_new) end  
   
20                          c1.add_child (c_new)                          c1.add_child (c_new)
21    
22                          check c1.is_wrapped and c2.is_wrapped end                          check c1.is_wrapped and c2.is_wrapped end

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

  ViewVC Help
Powered by ViewVC 1.1.23