/[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 93377 by julian, Wed Nov 13 08:05:21 2013 UTC revision 93378 by julian, Thu Nov 14 15:57:08 2013 UTC
# Line 17  feature Line 17  feature
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)
20    
21                            check c_new.parent = Void end
22                            check c_new.children_set.is_empty end
23    
24                            check not c1.up.has (c_new) end
25                            check not c1.children_set.has (c_new) end
26    
27                          c1.add_child (c_new)                          c1.add_child (c_new)
28    
29                          check c1.is_wrapped and c2.is_wrapped end                          check c1.is_wrapped and c2.is_wrapped end
30                          check c1.value >= c_new.value end                          check c1.value >= c_new.value end
31                  end                  end

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

  ViewVC Help
Powered by ViewVC 1.1.23