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

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

1 note
2 explicit: "all"
3
4 class F_I_ITERATOR_D
5
6 create
7 make
8
9 feature
10
11 target: F_I_COLLECTION_D
12
13 before, after: BOOLEAN
14
15 make (t: F_I_COLLECTION_D)
16 note
17 status: creator
18 require
19 is_open -- default: creator
20 t.is_wrapped -- default: creator
21 across t.observers as o all o.item.is_wrapped end -- default: creator
22 t /= Void
23
24 modify (Current)
25 modify_field ("observers", t)
26 do
27 target := t
28 before := True
29 t.unwrap
30 t.set_observers (t.observers & Current)
31 t.wrap
32 set_subjects ([t]) -- default: ?
33 wrap -- default: creator
34 ensure
35 target = t
36 t.observers = old t.observers & Current
37
38 t.elements = old t.elements -- t modified, t.elements in domain of t
39 t.elements.count = old t.elements.count -- t modified, t.elements in domain of t
40
41 before and not after
42 is_wrapped -- default: creator
43 across observers as o all o.item.is_wrapped end -- default: creator
44 t.is_wrapped -- default: creator
45 across t.observers as o all o.item.is_wrapped end -- default: creator
46 end
47
48 item: INTEGER
49 require
50 not (before or after)
51 target.is_wrapped
52 not is_open -- default: public
53 across observers as o all not o.item.is_open end -- default: public
54
55 modify ([]) -- default: query
56 do
57 Result := target.elements [index]
58 ensure
59 not is_open -- default: public
60 across observers as o all not o.item.is_open end -- default: public
61 target.is_wrapped
62 end
63
64 forth
65 require
66 not after
67 is_wrapped -- default: public
68 across observers as o all o.item.is_wrapped end -- default: public
69
70 modify ([Current]) -- default: command
71 do
72 unwrap -- default: public
73 index := index + 1
74 before := False
75 if index > target.count then
76 after := True
77 end
78 wrap -- default: public
79 ensure
80 not before
81 target = old target
82 -- target.observers = old target.observers
83 index = old index + 1
84 is_wrapped -- default: public
85 across observers as o all o.item.is_wrapped end -- default: public
86 end
87
88 feature -- Implementation
89
90 index: INTEGER
91
92 invariant
93 target /= Void
94 0 <= index and index <= target.count + 1
95 before = (index < 1)
96 after = (index > target.count)
97 subjects = [target]
98 across subjects as s all s.item.observers.has (Current) end -- default
99 observers = [] -- default
100 owns = [] -- default
101
102 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23