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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_client.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: 597 byte(s)
AutoProof: continued ownership implementation.

1 note
2 explicit: "all"
3
4 class F_COM_CLIENT
5
6 feature
7
8 test_d (c1, c2: F_COM_COMPOSITE_D)
9 require
10 c1.is_wrapped
11 c2.is_wrapped
12 across c1.up as o all o.item.is_wrapped end
13 across c1.observers as o all o.item.is_wrapped end
14
15 modify ([c1, c2])
16 local
17 c_new: F_COM_COMPOSITE_D
18 do
19 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)
28
29 check c1.is_wrapped and c2.is_wrapped end
30 check c1.value >= c_new.value end
31 end
32
33 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23