/[eiffelstudio]/branches/eth/eve/Src/library/base/elks/kernel/string/readable_string_8.e
ViewVC logotype

Contents of /branches/eth/eve/Src/library/base/elks/kernel/string/readable_string_8.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 92811 - (show annotations)
Fri Jul 26 04:35:53 2013 UTC (6 years, 2 months ago) by jasonw
File size: 22123 byte(s)
<<Merged from trunk#92810.>>
1 note
2 description: "[
3 Sequences of 8-bit characters, accessible through integer indices
4 in a contiguous range. Read-only interface.
5 ]"
6 library: "Free implementation of ELKS library"
7 status: "See notice at end of class."
8 legal: "See notice at end of class."
9 date: "$Date$"
10 revision: "$Revision$"
11
12 deferred class
13 READABLE_STRING_8
14
15 inherit
16 READABLE_STRING_GENERAL
17 rename
18 same_string as same_string_general,
19 same_characters as same_characters_general,
20 same_caseless_characters as same_caseless_characters_general,
21 starts_with as starts_with_general,
22 ends_with as ends_with_general,
23 is_case_insensitive_equal as is_case_insensitive_equal_general,
24 item as character_32_item,
25 has as character_32_has,
26 index_of as character_32_index_of,
27 last_index_of as character_32_last_index_of,
28 occurrences as character_32_occurrences
29 redefine
30 copy, is_equal, out
31 end
32
33 READABLE_INDEXABLE [CHARACTER_8]
34 redefine
35 copy, is_equal, out
36 end
37
38 convert
39 to_cil: {SYSTEM_STRING},
40 as_string_8: {STRING_8},
41 as_readable_string_32: {READABLE_STRING_32},
42 as_string_32: {STRING_32}
43
44 feature {NONE} -- Initialization
45
46 make (n: INTEGER)
47 -- Allocate space for at least `n' characters.
48 do
49 count := 0
50 internal_hash_code := 0
51 create area.make_filled ('%/000/', n + 1)
52 end
53
54 make_filled (c: CHARACTER_8; n: INTEGER)
55 -- Create string of length `n' filled with `c'.
56 require
57 valid_count: n >= 0
58 do
59 make (n)
60 fill_character (c)
61 ensure
62 count_set: count = n
63 area_allocated: capacity >= n
64 filled: occurrences (c) = count
65 end
66
67 make_from_string (s: READABLE_STRING_8)
68 -- Initialize from the characters of `s'.
69 require
70 string_exists: s /= Void
71 do
72 area := s.area
73 count := s.count
74 internal_hash_code := 0
75 if Current /= s then
76 create area.make_empty (count + 1)
77 area.copy_data (s.area, s.area_lower, 0, count + 1)
78 end
79 ensure
80 not_shared_implementation: Current /= s implies not shared_with (s)
81 initialized: same_string (s)
82 end
83
84 make_from_c (c_string: POINTER)
85 -- Initialize from contents of `c_string',
86 -- a string created by some C function
87 require
88 c_string_exists: c_string /= default_pointer
89 local
90 l_count: INTEGER
91 do
92 c_string_provider.set_shared_from_pointer (c_string)
93 l_count := c_string_provider.count
94 create area.make_filled ('%/000/', l_count + 1)
95 count := l_count
96 internal_hash_code := 0
97 c_string_provider.read_substring_into_character_8_area (area, 1, l_count)
98 end
99
100 make_from_c_pointer (c_string: POINTER)
101 -- Create new instance from contents of `c_string',
102 -- a string created by some C function
103 obsolete
104 "Use `make_from_c' instead."
105 require
106 c_string_exists: c_string /= default_pointer
107 do
108 make_from_c (c_string)
109 end
110
111 make_from_cil (a_system_string: detachable SYSTEM_STRING)
112 -- Initialize Current with `a_system_string'.
113 require
114 is_dotnet: {PLATFORM}.is_dotnet
115 deferred
116 end
117
118 make_from_separate (other: separate READABLE_STRING_8)
119 -- Initialize current string from `other'.
120 require
121 other_not_void: other /= Void
122 local
123 i, nb: INTEGER
124 l_area: like area
125 do
126 nb := other.count
127 make (nb)
128 from
129 l_area := area
130 i := 0
131 until
132 i = nb
133 loop
134 l_area.put (other.item (i + 1), i)
135 i := i + 1
136 end
137 count := nb
138 ensure
139 same_string: -- `other' and `Current' have the same content.
140 end
141
142 feature -- Access
143
144 item alias "[]", at alias "@" (i: INTEGER): CHARACTER_8
145 -- Character at position `i'.
146 deferred
147 end
148
149 item_code (i: INTEGER): INTEGER
150 -- Numeric code of character at position `i'.
151 obsolete
152 "For consistency with Unicode string handling, use `code (i)' instead."
153 require
154 index_small_enough: i <= count
155 index_large_enough: i > 0
156 deferred
157 end
158
159 shared_with (other: READABLE_STRING_8): BOOLEAN
160 -- Does string share the text of `other'?
161 do
162 Result := (other /= Void) and then (area = other.area)
163 end
164
165 index_of (c: CHARACTER_8; start_index: INTEGER): INTEGER
166 -- Position of first occurrence of `c' at or after `start_index';
167 -- 0 if none.
168 require
169 start_large_enough: start_index >= 1
170 start_small_enough: start_index <= count + 1
171 local
172 a: like area
173 i, nb, l_lower_area: INTEGER
174 do
175 nb := count
176 if start_index <= nb then
177 from
178 l_lower_area := area_lower
179 i := start_index - 1 + l_lower_area
180 nb := nb + l_lower_area
181 a := area
182 until
183 i = nb or else a.item (i) = c
184 loop
185 i := i + 1
186 end
187 if i < nb then
188 -- We add +1 due to the area starting at 0 and not at 1
189 -- and substract `area_lower'
190 Result := i + 1 - l_lower_area
191 end
192 end
193 ensure
194 valid_result: Result = 0 or (start_index <= Result and Result <= count)
195 zero_if_absent: (Result = 0) = not substring (start_index, count).has (c)
196 found_if_present: substring (start_index, count).has (c) implies item (Result) = c
197 none_before: substring (start_index, count).has (c) implies
198 not substring (start_index, Result - 1).has (c)
199 end
200
201 last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER): INTEGER
202 -- Position of last occurrence of `c',
203 -- 0 if none.
204 require
205 start_index_small_enough: start_index_from_end <= count
206 start_index_large_enough: start_index_from_end >= 1
207 local
208 a: like area
209 i, l_lower_area: INTEGER
210 do
211 from
212 l_lower_area := area_lower
213 i := start_index_from_end - 1 + l_lower_area
214 a := area
215 until
216 i < l_lower_area or else a.item (i) = c
217 loop
218 i := i - 1
219 end
220 -- We add +1 due to the area starting at 0 and not at 1.
221 Result := i + 1 - l_lower_area
222 ensure
223 valid_result: 0 <= Result and Result <= start_index_from_end
224 zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).has (c)
225 found_if_present: substring (1, start_index_from_end).has (c) implies item (Result) = c
226 none_after: substring (1, start_index_from_end).has (c) implies
227 not substring (Result + 1, start_index_from_end).has (c)
228 end
229
230 substring_index_in_bounds (other: READABLE_STRING_GENERAL; start_pos, end_pos: INTEGER): INTEGER
231 -- <Precursor>
232 do
233 Result := string_searcher.substring_index (Current, other, start_pos, end_pos)
234 end
235
236 string: STRING_8
237 -- New STRING_8 having same character sequence as `Current'.
238 do
239 create Result.make_from_string (Current)
240 ensure
241 string_not_void: Result /= Void
242 string_type: Result.same_type (create {STRING_8}.make_empty)
243 first_item: count > 0 implies Result.item (1) = item (1)
244 recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string
245 end
246
247 string_representation: STRING_8
248 -- Similar to `string' but only create a new object if `Current' is not of dynamic type {STRING_8}
249 do
250 if same_type (create {STRING_8}.make_empty) and then attached {STRING_8} Current as l_s8 then
251 Result := l_s8
252 else
253 Result := string
254 end
255 ensure
256 Result_not_void: Result /= Void
257 correct_type: Result.same_type (create {STRING_8}.make_empty)
258 first_item: count > 0 implies Result.item (1) = item (1)
259 recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string
260 end
261
262 substring_index (other: READABLE_STRING_GENERAL; start_index: INTEGER): INTEGER
263 -- <Precursor>
264 do
265 Result := string_searcher.substring_index (Current, other, start_index, count)
266 end
267
268 fuzzy_index (other: READABLE_STRING_GENERAL; start: INTEGER; fuzz: INTEGER): INTEGER
269 -- <Precursor>
270 do
271 Result := string_searcher.fuzzy_index (Current, other, start, count, fuzz)
272 end
273
274 feature -- Measurement
275
276 capacity: INTEGER
277 -- Allocated space
278 do
279 Result := area.count - 1
280 end
281
282 count: INTEGER
283 -- Actual number of characters making up the string
284
285 occurrences (c: CHARACTER_8): INTEGER
286 -- Number of times `c' appears in the string
287 local
288 i, nb: INTEGER
289 a: SPECIAL [CHARACTER_8]
290 do
291 from
292 i := area_lower
293 nb := count + i
294 a := area
295 until
296 i = nb
297 loop
298 if a.item (i) = c then
299 Result := Result + 1
300 end
301 i := i + 1
302 end
303 ensure then
304 zero_if_empty: count = 0 implies Result = 0
305 recurse_if_not_found_at_first_position:
306 (count > 0 and then item (1) /= c) implies
307 Result = substring (2, count).occurrences (c)
308 recurse_if_found_at_first_position:
309 (count > 0 and then item (1) = c) implies
310 Result = 1 + substring (2, count).occurrences (c)
311 end
312
313 index_set: INTEGER_INTERVAL
314 -- Range of acceptable indexes
315 do
316 create Result.make (1, count)
317 ensure then
318 index_set_not_void: Result /= Void
319 index_set_count: Result.count = count
320 end
321
322 feature -- Comparison
323
324 is_equal (other: like Current): BOOLEAN
325 -- Is string made of same character sequence as `other'
326 -- (possibly with a different capacity)?
327 local
328 nb: INTEGER
329 l_hash, l_other_hash: like internal_hash_code
330 do
331 if other = Current then
332 Result := True
333 else
334 nb := count
335 if nb = other.count then
336 -- Let's compare the content if and only if the hash_code are the same or not yet computed.
337 l_hash := internal_hash_code
338 l_other_hash := other.internal_hash_code
339 if l_hash = 0 or else l_other_hash = 0 or else l_hash = l_other_hash then
340 Result := area.same_items (other.area, other.area_lower, area_lower, nb)
341 end
342 end
343 end
344 end
345
346 is_case_insensitive_equal (other: READABLE_STRING_8): BOOLEAN
347 -- Is string made of same character sequence as `other' regardless of casing
348 -- (possibly with a different capacity)?
349 require
350 other_not_void: other /= Void
351 local
352 nb: INTEGER
353 do
354 if other = Current then
355 Result := True
356 else
357 nb := count
358 if nb = other.count then
359 Result := nb = 0 or else same_caseless_characters (other, 1, nb, 1)
360 end
361 end
362 ensure
363 symmetric: Result implies other.is_case_insensitive_equal (Current)
364 consistent: attached {like Current} other as l_other implies (standard_is_equal (l_other) implies Result)
365 valid_result: as_lower ~ other.as_lower implies Result
366 end
367
368 same_caseless_characters (other: READABLE_STRING_8; start_pos, end_pos, index_pos: INTEGER): BOOLEAN
369 -- Are characters of `other' within bounds `start_pos' and `end_pos'
370 -- caseless identical to characters of current string starting at index `index_pos'.
371 require
372 other_not_void: other /= Void
373 valid_start_pos: other.valid_index (start_pos)
374 valid_end_pos: other.valid_index (end_pos)
375 valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
376 valid_index_pos: valid_index (index_pos)
377 local
378 i, j, nb: INTEGER
379 l_area, l_other_area: like area
380 c1,c2: CHARACTER
381 do
382 nb := end_pos - start_pos + 1
383 if nb <= count - index_pos + 1 then
384 from
385 l_area := area
386 l_other_area := other.area
387 Result := True
388 i := area_lower + index_pos - 1
389 j := other.area_lower + start_pos - 1
390 nb := nb + i
391 until
392 i = nb
393 loop
394 c1 := l_area.item (i)
395 c2 := l_other_area.item (j)
396 if c1 /= c2 and then c1.as_lower /= c2.as_lower then
397 Result := False
398 i := nb - 1 -- Jump out of the loop
399 end
400 i := i + 1
401 j := j + 1
402 variant
403 increasing_index: l_area.upper - i + 1
404 end
405 end
406 ensure
407 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal (other.substring (start_pos, end_pos))
408 end
409
410 same_string (other: READABLE_STRING_8): BOOLEAN
411 -- Do `Current' and `other' have same character sequence?
412 require
413 other_not_void: other /= Void
414 local
415 nb: INTEGER
416 do
417 if other = Current then
418 Result := True
419 else
420 nb := count
421 if nb = other.count then
422 Result := nb = 0 or else same_characters (other, 1, nb, 1)
423 end
424 end
425 ensure
426 definition: Result = (string ~ other.string)
427 end
428
429 same_characters (other: READABLE_STRING_8; start_pos, end_pos, index_pos: INTEGER): BOOLEAN
430 -- Are characters of `other' within bounds `start_pos' and `end_pos'
431 -- identical to characters of current string starting at index `index_pos'.
432 require
433 other_not_void: other /= Void
434 valid_start_pos: other.valid_index (start_pos)
435 valid_end_pos: other.valid_index (end_pos)
436 valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
437 valid_index_pos: valid_index (index_pos)
438 local
439 nb: INTEGER
440 do
441 nb := end_pos - start_pos + 1
442 if nb <= count - index_pos + 1 then
443 Result := area.same_items (other.area, other.area_lower + start_pos - 1, area_lower + index_pos - 1, nb)
444 end
445 ensure
446 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string (other.substring (start_pos, end_pos))
447 end
448
449 is_less alias "<" (other: like Current): BOOLEAN
450 -- Is string lexicographically lower than `other'?
451 local
452 other_count: INTEGER
453 current_count: INTEGER
454 do
455 if other /= Current then
456 other_count := other.count
457 current_count := count
458 if other_count = current_count then
459 Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, other_count) > 0
460 else
461 if current_count < other_count then
462 Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, current_count) >= 0
463 else
464 Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, other_count) > 0
465 end
466 end
467 end
468 end
469
470 feature -- Status report
471
472 is_string_8: BOOLEAN = True
473 -- <Precursor>
474
475 is_string_32: BOOLEAN = False
476 -- <Precursor>
477
478 is_valid_as_string_8: BOOLEAN = True
479 -- <Precursor>
480
481 has (c: CHARACTER_8): BOOLEAN
482 -- Does string include `c'?
483 local
484 i, nb: INTEGER
485 l_area: like area
486 do
487 nb := count
488 if nb > 0 then
489 from
490 i := area_lower
491 l_area := area
492 nb := nb + i
493 until
494 i = nb or else (l_area.item (i) = c)
495 loop
496 i := i + 1
497 end
498 Result := (i < nb)
499 end
500 ensure then
501 false_if_empty: count = 0 implies not Result
502 true_if_first: count > 0 and then item (1) = c implies Result
503 recurse: (count > 0 and then item (1) /= c) implies
504 (Result = substring (2, count).has (c))
505 end
506
507 starts_with (s: READABLE_STRING_8): BOOLEAN
508 -- Does string begin with `s'?
509 require
510 argument_not_void: s /= Void
511 local
512 i, j, nb: INTEGER
513 l_area, l_s_area: like area
514 do
515 if Current = s then
516 Result := True
517 else
518 i := s.count
519 if i <= count then
520 from
521 l_area := area
522 l_s_area := s.area
523 j := area_lower + i
524 i := s.area_upper + 1
525 nb := s.area_lower
526 Result := True
527 until
528 i = nb
529 loop
530 i := i - 1
531 j := j - 1
532 if l_area.item (j) /= l_s_area.item (i) then
533 Result := False
534 i := nb -- Jump out of loop
535 end
536 end
537 end
538 end
539 ensure
540 definition: Result = s.same_string (substring (1, s.count))
541 end
542
543 ends_with (s: READABLE_STRING_8): BOOLEAN
544 -- Does string finish with `s'?
545 require
546 argument_not_void: s /= Void
547 local
548 i, j, nb: INTEGER
549 l_area, l_s_area: like area
550 do
551 if Current = s then
552 Result := True
553 else
554 i := s.count
555 j := count
556 if i <= j then
557 from
558 l_area := area
559 l_s_area := s.area
560 j := area_upper + 1
561 i := s.area_upper + 1
562 nb := s.area_lower
563 Result := True
564 until
565 i = nb
566 loop
567 i := i - 1
568 j := j - 1
569 if l_area.item (j) /= l_s_area.item (i) then
570 Result := False
571 i := nb -- Jump out of loop
572 end
573 end
574 end
575 end
576 ensure
577 definition: Result = s.same_string (substring (count - s.count + 1, count))
578 end
579
580 valid_code (v: NATURAL_32): BOOLEAN
581 -- Is `v' a valid code for a CHARACTER_32?
582 do
583 Result := v <= {CHARACTER_8}.max_value.to_natural_32
584 end
585
586 is_boolean: BOOLEAN
587 -- Does `Current' represent a BOOLEAN?
588 local
589 nb: INTEGER
590 l_area: like area
591 i: INTEGER
592 do
593 nb := count
594 if nb = 4 then
595 -- Check if this is `true_constant'
596 l_area := area
597 i := area_lower
598 Result := l_area.item (i).lower = 't' and then
599 l_area.item (i + 1).lower = 'r' and then
600 l_area.item (i + 2).lower = 'u' and then
601 l_area.item (i + 3).lower = 'e'
602 elseif nb = 5 then
603 -- Check if this is `false_constant'
604 l_area := area
605 i := area_lower
606 Result := l_area.item (i).lower = 'f' and then
607 l_area.item (i + 1).lower = 'a' and then
608 l_area.item (i + 2).lower = 'l' and then
609 l_area.item (i + 3).lower = 's' and then
610 l_area.item (i + 4).lower = 'e'
611 end
612 end
613
614 feature {READABLE_STRING_8} -- Duplication
615
616 copy (other: like Current)
617 -- Reinitialize by copying the characters of `other'.
618 -- (This is also used by `twin'.)
619 local
620 old_area: like area
621 do
622 if other /= Current then
623 old_area := area
624 standard_copy (other)
625 -- Note: <= is needed as all Eiffel string should have an
626 -- extra character to insert null character at the end.
627 if old_area = Void or else old_area = other.area or else old_area.count <= count then
628 -- Prevent copying of large `area' if only a few characters are actually used.
629 area := area.resized_area (count + 1)
630 else
631 old_area.copy_data (area, 0, 0, count)
632 area := old_area
633 end
634 internal_hash_code := 0
635 end
636 ensure then
637 new_result_count: count = other.count
638 -- same_characters: For every `i' in 1..`count', `item' (`i') = `other'.`item' (`i')
639 end
640
641 feature {NONE} -- Element change
642
643 fill_character (c: CHARACTER_8)
644 -- Fill with `capacity' characters all equal to `c'.
645 local
646 l_cap: like capacity
647 do
648 l_cap := capacity
649 if l_cap /= 0 then
650 area.fill_with (c, 0, l_cap - 1)
651 count := l_cap
652 internal_hash_code := 0
653 end
654 ensure
655 filled: count = capacity
656 same_size: capacity = old capacity
657 -- all_char: For every `i' in 1..`capacity', `item' (`i') = `c'
658 end
659
660 feature -- Conversion
661
662 mirrored: like Current
663 -- Mirror image of string;
664 -- Result for "Hello world" is "dlrow olleH".
665 deferred
666 ensure
667 same_count: Result.count = count
668 -- reversed: For every `i' in 1..`count', `Result'.`item' (`i') = `item' (`count'+1-`i')
669 end
670
671 feature -- Duplication
672
673 substring (start_index, end_index: INTEGER): like Current
674 -- Copy of substring containing all characters at indices
675 -- between `start_index' and `end_index'
676 deferred
677 end
678
679 feature -- Output
680
681 out: STRING
682 -- Printable representation
683 do
684 create Result.make (count)
685 Result.append (Current)
686 ensure then
687 out_not_void: Result /= Void
688 same_items: same_type ("") implies Result.same_string (Current)
689 end
690
691 feature {NONE} -- Implementation
692
693 string_searcher: STRING_8_SEARCHER
694 -- String searcher specialized for READABLE_STRING_8 instances
695 once
696 create Result.make
697 end
698
699 str_strict_cmp (this, other: like area; this_index, other_index, n: INTEGER): INTEGER
700 -- Compare `n' characters from `this' starting at `this_index' with
701 -- `n' characters from and `other' starting at `other_index'.
702 -- 0 if equal, < 0 if `this' < `other',
703 -- > 0 if `this' > `other'
704 require
705 this_not_void: this /= Void
706 other_not_void: other /= Void
707 n_non_negative: n >= 0
708 n_valid: n <= (this.upper - this_index + 1) and n <= (other.upper - other_index + 1)
709 local
710 i, j, nb, l_current_code, l_other_code: INTEGER
711 do
712 from
713 i := this_index
714 nb := i + n
715 j := other_index
716 until
717 i = nb
718 loop
719 l_current_code := this.item (i).code
720 l_other_code := other.item (j).code
721 if l_current_code /= l_other_code then
722 Result := l_current_code - l_other_code
723 i := nb - 1 -- Jump out of loop
724 end
725 i := i + 1
726 j := j + 1
727 end
728 end
729
730 to_lower_area (a: like area; start_index, end_index: INTEGER)
731 -- Replace all characters in `a' between `start_index' and `end_index'
732 -- with their lower version.
733 require
734 a_not_void: a /= Void
735 start_index_non_negative: start_index >= 0
736 start_index_not_too_big: start_index <= end_index + 1
737 end_index_valid: end_index < a.count
738 local
739 i: INTEGER
740 do
741 from
742 i := start_index
743 until
744 i > end_index
745 loop
746 a.put (a.item (i).lower, i)
747 i := i + 1
748 end
749 end
750
751 to_upper_area (a: like area; start_index, end_index: INTEGER)
752 -- Replace all characters in `a' between `start_index' and `end_index'
753 -- with their upper version.
754 require
755 a_not_void: a /= Void
756 start_index_non_negative: start_index >= 0
757 start_index_not_too_big: start_index <= end_index + 1
758 end_index_valid: end_index < a.count
759 local
760 i: INTEGER
761 do
762 from
763 i := start_index
764 until
765 i > end_index
766 loop
767 a.put (a.item (i).upper, i)
768 i := i + 1
769 end
770 end
771
772 mirror_area (a: like area; start_index, end_index: INTEGER)
773 -- Mirror all characters in `a' between `start_index' and `end_index'.
774 require
775 a_not_void: a /= Void
776 start_index_non_negative: start_index >= 0
777 start_index_not_too_big: start_index <= end_index + 1
778 end_index_valid: end_index < a.count
779 local
780 c: CHARACTER_8
781 i, j: INTEGER
782 do
783 from
784 i := end_index
785 until
786 i <= j
787 loop
788 c := a.item (i)
789 a.put (a.item (j), i)
790 a.put (c, j)
791 i := i - 1
792 j := j + 1
793 end
794 end
795
796 feature
797 {READABLE_STRING_8, READABLE_STRING_32,
798 STRING_8_SEARCHER, STRING_32_SEARCHER,
799 HEXADECIMAL_STRING_TO_INTEGER_CONVERTER,
800 STRING_TO_INTEGER_CONVERTOR,
801 STRING_TO_REAL_CONVERTOR} -- Implementation
802
803 area: SPECIAL [CHARACTER_8]
804 -- Storage for characters
805
806 area_lower: INTEGER
807 -- Minimum index
808 do
809 ensure
810 area_lower_non_negative: Result >= 0
811 area_lower_valid: Result <= area.upper
812 end
813
814 area_upper: INTEGER
815 -- Maximum index
816 do
817 Result := area_lower + count - 1
818 ensure
819 area_upper_valid: Result <= area.upper
820 area_upper_in_bound: area_lower <= Result + 1
821 end
822
823 invariant
824 area_not_void: area /= Void
825
826 note
827 copyright: "Copyright (c) 1984-2013, Eiffel Software and others"
828 license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
829 source: "[
830 Eiffel Software
831 5949 Hollister Ave., Goleta, CA 93117 USA
832 Telephone 805-685-1006, Fax 805-685-6869
833 Website http://www.eiffel.com
834 Customer support http://support.eiffel.com
835 ]"
836
837 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23