/[eiffelstudio]/branches/eth/eve/Src/library/base/base2/iterator/v_io_iterator.e
ViewVC logotype

Annotation of /branches/eth/eve/Src/library/base/base2/iterator/v_io_iterator.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94771 - (hide annotations)
Thu Apr 3 12:37:44 2014 UTC (5 years, 9 months ago) by polikarn
File size: 1906 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
1 polikarn 94288 note
2     description: "Iterators to read and write from/to a container in linear order."
3     author: "Nadia Polikarpova"
4 polikarn 94492 model: target, sequence, index_
5 polikarn 94288
6     deferred class
7     V_IO_ITERATOR [G]
8    
9     inherit
10     V_ITERATOR [G]
11 polikarn 94461 redefine
12 polikarn 94771 index_,
13     start
14 polikarn 94461 end
15 polikarn 94288
16     V_OUTPUT_STREAM [G]
17     undefine
18     is_equal
19     end
20    
21 polikarn 94461 feature -- Measurement
22    
23 polikarn 94492 index_: INTEGER
24 polikarn 94461 -- Current position.
25     note
26 polikarn 94604 status: ghost
27 polikarn 94461 replaces: off_
28     attribute
29     end
30    
31 polikarn 94288 feature -- Replacement
32    
33 polikarn 94771 start
34     -- Go to the first position.
35     require else
36     modify_model ("off_", Current)
37     deferred
38     end
39    
40 polikarn 94288 put (v: G)
41     -- Replace item at current position with `v'.
42     require
43     not_off: not off
44     target_wrapped: target.is_wrapped
45 polikarn 94582 other_observers_open: across target.observers as o all o.item /= Current implies o.item.is_open end
46 polikarn 94332 modify_model (["sequence"], Current)
47     modify_model (["bag"], target)
48 polikarn 94288 deferred
49     ensure
50 polikarn 94492 sequence_effect: sequence ~ old sequence.replaced_at (index_, v)
51 polikarn 94288 target_wrapped: target.is_wrapped
52 polikarn 94492 target_bag_effect: target.bag ~ old ((target.bag / sequence [index_]) & v)
53 polikarn 94288 end
54    
55     output (v: G)
56     -- Replace item at current position with `v' and go to the next position.
57     note
58     explicit: wrapping
59     require else
60 polikarn 94492 modify_model (["sequence", "index_"], Current)
61 polikarn 94288 do
62 polikarn 94603 check inv_only ("subjects_definition", "subjects_contraint") end
63 polikarn 94288 put (v)
64     forth
65     ensure then
66 polikarn 94492 sequence_effect: sequence ~ old (sequence.replaced_at (index_, v))
67     index_effect: index_ = old index_ + 1
68 polikarn 94288 end
69    
70     invariant
71 polikarn 94492 off_definition: off_ = not sequence.domain [index_]
72 polikarn 94288
73     note
74     copyright: "Copyright (c) 1984-2014, Eiffel Software and others"
75     license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
76     source: "[
77     Eiffel Software
78     5949 Hollister Ave., Goleta, CA 93117 USA
79     Telephone 805-685-1006, Fax 805-685-6869
80     Website http://www.eiffel.com
81     Customer support http://support.eiffel.com
82     ]"
83     end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23