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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_many/f_oom_observer_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: 1290 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: "Observer that needs to maintain a cache of its subject's state."
3 explicit: "all"
4
5 class F_OOM_OBSERVER_D
6
7 create
8 make
9
10 feature {NONE} -- Initialization
11
12 make (s: F_OOM_SUBJECT_D)
13 -- Create an observer subscribed to `s'.
14 note
15 status: creator
16 require
17 s_exists: s /= Void
18 default_arg_wrapped: s.is_wrapped
19 modify (s, Current)
20 do
21 subject := s
22 s.register (Current)
23 cache := s.value
24 set_subjects ([subject])
25 wrap
26 ensure
27 subject_set: subject = s
28 observeing_subject: s.observers = old s.observers & Current
29 default_wrapped: is_wrapped
30 default_arg_wrapped: s.is_wrapped
31 end
32
33 feature -- Public access
34
35 subject: F_OOM_SUBJECT_D
36 -- Subject.
37
38 cache: INTEGER
39 -- Copy of subject's state.
40
41 feature {F_OOM_SUBJECT_D} -- Internal communication
42
43 notify
44 -- Update `cache' according to the state `subject'.
45 require
46 open: is_open
47 partially_holds: inv_without ("cache_synchronized")
48 modify_field ("cache", Current)
49 do
50 cache := subject.value
51 ensure
52 invariant_holds: inv
53 end
54
55 invariant
56 subject_exists: subject /= Void
57 subject_aware: subject.observers.has (Current)
58 cache_synchronized: cache = subject.value
59 subjects_structure: subjects = [subject]
60 default: owns = []
61 default: observers = []
62 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23