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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_one/f_ooo_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: 1076 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 explicit: "all"
3
4 class F_OOO_OBSERVER_D
5
6 create
7 make
8
9 feature
10
11 make (s: F_OOO_SUBJECT_D)
12 note
13 status: creator
14 require
15 s.observer = Void
16 s.is_wrapped -- default: public
17
18 modify (s)
19 modify (Current) -- default: creator
20 do
21 subject := s
22 s.register (Current)
23 check s.inv end
24 cache := s.value
25
26 set_subjects ([subject])
27 wrap -- default: public/creator
28 ensure
29 subject = s
30 is_wrapped -- default: public/creator
31 s.is_wrapped -- default: public
32 end
33
34 feature -- Access
35
36 cache: INTEGER
37 -- Cached value of subject.
38
39 subject: F_OOO_SUBJECT_D
40 -- Subject of this observer.
41
42 feature {F_OOO_SUBJECT_D} -- Element change
43
44 notify
45 require
46 is_open
47 inv_without ("cache_synchronized")
48
49 modify_field ("cache", Current)
50 do
51 cache := subject.value
52 ensure
53 inv
54 end
55
56 invariant
57 attached subject
58 subject.observer = Current
59 cache_synchronized: cache = subject.value
60 subjects = [subject]
61 across subjects as sc all sc.item.observers.has (Current) end -- default
62 owns = [] -- default
63 observers = [] -- default
64
65 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23