/[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 93733 - (show annotations)
Mon Dec 16 12:32:04 2013 UTC (5 years, 10 months ago) by polikarn
File size: 1967 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: "An iterator to traverse collections."
3 exlipit: "all"
4
5 class F_I_ITERATOR_D
6
7 create
8 make
9
10 feature {NONE} -- Initialization
11
12 make (t: F_I_COLLECTION_D)
13 -- Create an iterator to traverse `t'.
14 note
15 status: creator
16 require
17 target_exists: t /= Void
18 default_arg_wrapped: t.is_wrapped
19 modify (Current)
20 modify_field (["observers", "closed"], t)
21 do
22 target := t
23 before := True
24 t.unwrap
25 t.set_observers (t.observers & Current)
26 t.wrap
27 set_subjects ([t])
28 ensure
29 target_set: target = t
30 before: before and not after
31 observing_target: t.observers = old t.observers & Current
32 capacity_unchanged: t.capacity = old t.capacity
33 default_wrapped: is_wrapped
34 default_arg_wrapped: t.is_wrapped
35 end
36
37 feature -- Access
38
39 target: F_I_COLLECTION_D
40 -- Collection to traverse.
41
42 before: BOOLEAN
43 -- Is the iterator before the first element?
44
45 after: BOOLEAN
46 -- Is the iterator after the last element?
47
48 item: INTEGER
49 -- Collection element at current position.
50 require
51 not_off: not (before or after)
52 target_closed: target.closed
53 default_closed: closed
54 modify ([])
55 do
56 check inv and target.inv end
57 Result := target.elements [index]
58 end
59
60 feature -- State change
61
62 forth
63 -- Move to the next position.
64 require
65 not_after: not after
66 default_wrapped: is_wrapped
67 modify ([Current])
68 do
69 index := index + 1
70 before := False
71 if index > target.count then
72 after := True
73 end
74 ensure
75 not_before: not before
76 target_unchanged: target = old target
77 default_wrapped: is_wrapped
78 end
79
80 feature {NONE} -- Implementation
81
82 index: INTEGER
83 -- Iterator position.
84
85 invariant
86 target_exists: target /= Void
87 index_in_bounds: 0 <= index and index <= target.count + 1
88 before_definition: before = (index < 1)
89 after_definition: after = (index > target.count)
90 subjects_structure: subjects = [target]
91 default_owns: owns = []
92 default_observers: observers = []
93
94 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23