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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_many/f_oom_subject_d.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93733 - (show annotations)
Mon Dec 16 12:32:04 2013 UTC (5 years, 10 months ago) by polikarn
File size: 2319 byte(s)
Changed handling of default initialization in creators: free preconditions instead of assignment; precondition is_open now cannot be disabled since there is no choice.
1 note
2 description: "Subject that keeps a list of subscribers and nofifies then of its state changes."
3 explicit: "all"
4
5 class F_OOM_SUBJECT_D
6
7 create
8 make
9
10 feature {NONE} -- Initialization
11
12 make (v: INTEGER)
13 -- Create a subject with state `v' and no subscribers.
14 note
15 status: creator
16 require
17 modify (Current)
18 do
19 value := v
20 create subscribers.make
21 set_owns ([subscribers])
22 wrap
23 ensure
24 value_set: value = v
25 no_subscribers: subscribers.is_empty
26 default_wrapped: is_wrapped
27 default_observers_wrapped: across observers as o all o.item.is_wrapped end
28 end
29
30 feature -- Public access
31
32 value: INTEGER
33 -- State.
34
35 subscribers: F_OOM_LIST [F_OOM_OBSERVER_D]
36 -- List of observers subscribed to the state updates.
37
38 feature -- State update
39
40 update (v: INTEGER)
41 -- Update state to `v'.
42 require
43 default_wrapped: is_wrapped
44 default_observers_wrapped: across observers as o all o.item.is_wrapped end
45 modify_field (["value", "closed"], Current)
46 modify_field (["cache", "closed"], subscribers.sequence)
47 local
48 i: INTEGER
49 do
50 unwrap
51 unwrap_all (observers)
52 value := v
53
54 from
55 i := 1
56 invariant
57 subscribers.is_wrapped
58 across subscribers.sequence as o all
59 o.item.is_open and o.item.inv_without ("cache_synchronized")
60 end
61 across 1 |..| (i - 1) as j all subscribers.sequence [j.item].inv end
62 inv
63 value = v
64 until
65 i > subscribers.count
66 loop
67 subscribers [i].notify
68 i := i + 1
69 end
70
71 wrap_all (observers)
72 wrap
73 ensure
74 value_set: value = v
75 default_wrapped: is_wrapped
76 default_observers_wrapped: across observers as o all o.item.is_wrapped end
77 end
78
79 feature {F_OOM_OBSERVER_D} -- Internal communication
80
81 register (o: F_OOM_OBSERVER_D)
82 -- Add `o' to `subscribers'.
83 require
84 wrapped: is_wrapped
85 o_open: o.is_open
86 modify ([Current])
87 do
88 unwrap
89 subscribers.extend_back (o)
90 set_observers (observers + [o])
91 wrap
92 ensure
93 observers_extended: observers = old observers & o
94 wrapped: is_wrapped
95 end
96
97 invariant
98 subscribers_exists: subscribers /= Void
99 all_subscribers_exist: across subscribers.sequence as o all attached o.item end
100 observers_structure: observers = subscribers.sequence.range
101 owns_structure: owns = [subscribers]
102 subjects_structure: subjects = []
103
104 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23