/[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 93405 - (show annotations)
Fri Nov 15 21:07:40 2013 UTC (5 years, 11 months ago) by julian
File size: 464 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, c1.up, c1.children_set])
16 local
17 c_new: F_COM_COMPOSITE_D
18 do
19 create c_new.make (10)
20 c1.add_child (c_new)
21
22 check c1.is_wrapped and c2.is_wrapped end
23 check c1.value >= c_new.value end
24 end
25
26 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23